Optics/ROOT at main · isabelle-utp/Optics · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
(******************************************************************************)
(* 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" (AFP) = "HOL-Eisbach" +
  options [timeout = 600]
  sessions
    "HOL-Library"
    "HOL-Algebra"
  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"