(******************************************************************************)
(* Project: The Optics Library                                                *)
(* File: ROOT                                                                 *)
(* Authors: Simon Foster (University of York, UK)                             *)
(* Emails: simon.foster@york.ac.uk                                            *)
(******************************************************************************)

(* Optics Library *)

chapter AFP

session "Optics" = "HOL-Eisbach" +
  options [timeout = 600]
  sessions
    "HOL-Library"
  theories
    Interp
    Two
    Lens_Laws
    Lens_Algebra
    Lens_Order
    Lens_Instances
    Lens_Symmetric
    Lenses
    Prisms
    Channel_Type
    Dataspace
    Scenes
    Optics
  theories [document = false]
    Lens_Record_Example
  theories
    Lens_State
  document_files
    "root.bib"
    "root.tex"
    "document.sty"
    "figures/Lens.pdf"
    "figures/Composition.pdf"
    "figures/Sum.pdf"
    "figures/Independence.pdf"