1chapter HOL
2
3session HOL (main) = Pure +
4  description "
5    Classical Higher-order Logic.
6  "
7  options [strict_facts]
8  sessions Tools
9  theories
10    Main (global)
11    Complex_Main (global)
12  document_files
13    "root.bib"
14    "root.tex"
15
16session "HOL-Proofs" (timing) in Proofs = Pure +
17  description "
18    HOL-Main with explicit proof terms.
19  "
20  options [quick_and_dirty = false, record_proofs = 2, parallel_limit = 500]
21  sessions
22    "HOL-Library"
23  theories
24    "HOL-Library.Realizers"
25
26session "HOL-Library" (main timing) in Library = HOL +
27  description "
28    Classical Higher-order Logic -- batteries included.
29  "
30  theories
31    Library
32    (*conflicting type class instantiations and dependent applications*)
33    Finite_Lattice
34    List_Lexorder
35    Prefix_Order
36    Product_Lexorder
37    Product_Order
38    Subseq_Order
39    (*conflicting syntax*)
40    Datatype_Records
41    (*data refinements and dependent applications*)
42    AList_Mapping
43    Code_Binary_Nat
44    Code_Prolog
45    Code_Real_Approx_By_Float
46    Code_Target_Numeral
47    DAList
48    DAList_Multiset
49    RBT_Mapping
50    RBT_Set
51    (*printing modifications*)
52    OptionalSugar
53    (*prototypic tools*)
54    Predicate_Compile_Quickcheck
55    Quantified_Premise_Simproc
56    (*legacy tools*)
57    Old_Datatype
58    Old_Recdef
59    Realizers
60    Refute
61  document_files "root.bib" "root.tex"
62
63session "HOL-Analysis" (main timing) in Analysis = HOL +
64  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
65    document_variants = "document:manual=-proof,-ML,-unimportant"]
66  sessions
67    "HOL-Library"
68    "HOL-Computational_Algebra"
69  theories
70    Analysis
71  document_files
72    "root.tex"
73    "root.bib"
74
75session "HOL-Complex_Analysis" (main timing) in Complex_Analysis = "HOL-Analysis" +
76  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
77    document_variants = "document:manual=-proof,-ML,-unimportant"]
78  theories
79    Complex_Analysis
80  document_files
81    "root.tex"
82    "root.bib"
83
84session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" +
85  theories
86    Approximations
87    Metric_Arith_Examples
88
89session "HOL-Homology" (timing) in Homology = "HOL-Analysis" +
90  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
91    document_variants = "document:manual=-proof,-ML,-unimportant"]
92  sessions
93    "HOL-Algebra"
94  theories
95    Homology
96  document_files
97    "root.tex"
98
99session "HOL-Computational_Algebra" (main timing) in "Computational_Algebra" = "HOL-Library" +
100  theories
101    Computational_Algebra
102    (*conflicting type class instantiations and dependent applications*)
103    Field_as_Ring
104
105session "HOL-Real_Asymp" in Real_Asymp = HOL +
106  sessions
107    "HOL-Decision_Procs"
108  theories
109    Real_Asymp
110    Real_Asymp_Approx
111    Real_Asymp_Examples
112
113session "HOL-Real_Asymp-Manual" in "Real_Asymp/Manual" = "HOL-Real_Asymp" +
114  theories
115    Real_Asymp_Doc
116  document_files (in "~~/src/Doc")
117    "iman.sty"
118    "extra.sty"
119    "isar.sty"
120  document_files
121    "root.tex"
122    "style.sty"
123
124session "HOL-Hahn_Banach" in Hahn_Banach = "HOL-Library" +
125  description "
126    Author:     Gertrud Bauer, TU Munich
127
128    The Hahn-Banach theorem for real vector spaces.
129
130    This is the proof of the Hahn-Banach theorem for real vectorspaces,
131    following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach
132    theorem is one of the fundamental theorems of functional analysis. It is a
133    conclusion of Zorn's lemma.
134
135    Two different formaulations of the theorem are presented, one for general
136    real vectorspaces and its application to normed vectorspaces.
137
138    The theorem says, that every continous linearform, defined on arbitrary
139    subspaces (not only one-dimensional subspaces), can be extended to a
140    continous linearform on the whole vectorspace.
141  "
142  sessions
143    "HOL-Analysis"
144  theories
145    Hahn_Banach
146  document_files "root.bib" "root.tex"
147
148session "HOL-Induct" in Induct = "HOL-Library" +
149  description "
150    Examples of (Co)Inductive Definitions.
151
152    Comb proves the Church-Rosser theorem for combinators (see
153    http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz).
154
155    Mutil is the famous Mutilated Chess Board problem (see
156    http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz).
157
158    PropLog proves the completeness of a formalization of propositional logic
159    (see
160    http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz).
161
162    Exp demonstrates the use of iterated inductive definitions to reason about
163    mutually recursive relations.
164  "
165  theories [quick_and_dirty]
166    Common_Patterns
167  theories
168    Nested_Datatype
169    QuoDataType
170    QuoNestedDataType
171    Term
172    SList
173    ABexp
174    Infinitely_Branching_Tree
175    Ordinals
176    Sigma_Algebra
177    Comb
178    PropLog
179    Com
180  document_files "root.tex"
181
182session "HOL-IMP" (timing) in IMP = "HOL-Library" +
183  options [document_variants = document]
184  theories
185    BExp
186    ASM
187    Finite_Reachable
188    Denotational
189    Compiler2
190    Poly_Types
191    Sec_Typing
192    Sec_TypingT
193    Def_Init_Big
194    Def_Init_Small
195    Fold
196    Live
197    Live_True
198    Hoare_Examples
199    Hoare_Sound_Complete
200    VCG
201    Hoare_Total
202    VCG_Total_EX
203    VCG_Total_EX2
204    Collecting1
205    Collecting_Examples
206    Abs_Int_Tests
207    Abs_Int1_parity
208    Abs_Int1_const
209    Abs_Int3
210    Procs_Dyn_Vars_Dyn
211    Procs_Stat_Vars_Dyn
212    Procs_Stat_Vars_Stat
213    C_like
214    OO
215  document_files "root.bib" "root.tex"
216
217session "HOL-IMPP" in IMPP = HOL +
218  description \<open>
219    Author:     David von Oheimb
220    Copyright   1999 TUM
221
222    IMPP -- An imperative language with procedures.
223
224    This is an extension of IMP with local variables and mutually recursive
225    procedures. For documentation see "Hoare Logic for Mutual Recursion and
226    Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
227  \<close>
228  theories EvenOdd
229
230session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
231  options [document_variants = document]
232  sessions
233    "HOL-Number_Theory"
234  theories [document = false]
235    Less_False
236  theories
237    Sorting
238    Balance
239    Tree_Map
240    Interval_Tree
241    AVL_Map
242    RBT_Set2
243    RBT_Map
244    Tree23_Map
245    Tree234_Map
246    Brother12_Map
247    AA_Map
248    Set2_Join_RBT
249    Array_Braun
250    Trie_Fun
251    Trie_Map
252    Tries_Binary
253    Leftist_Heap
254    Binomial_Heap
255  document_files "root.tex" "root.bib"
256
257session "HOL-Import" in Import = HOL +
258  theories HOL_Light_Maps
259  theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
260
261session "HOL-Number_Theory" (main timing) in Number_Theory = "HOL-Computational_Algebra" +
262  description "
263    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
264    Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
265  "
266  sessions
267    "HOL-Algebra"
268  theories
269    Number_Theory
270  document_files
271    "root.tex"
272
273session "HOL-Hoare" in Hoare = HOL +
274  description "
275    Verification of imperative programs (verification conditions are generated
276    automatically from pre/post conditions and loop invariants).
277  "
278  theories Hoare
279  document_files "root.bib" "root.tex"
280
281session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL +
282  description "
283    Verification of shared-variable imperative programs a la Owicki-Gries.
284    (verification conditions are generated automatically).
285  "
286  theories Hoare_Parallel
287  document_files "root.bib" "root.tex"
288
289session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Number_Theory" +
290  sessions
291    "HOL-Data_Structures"
292    "HOL-ex"
293  theories
294    Generate
295    Generate_Binary_Nat
296    Generate_Target_Nat
297    Generate_Efficient_Datastructures
298    Code_Lazy_Test
299    Code_Test_PolyML
300    Code_Test_Scala
301  theories [condition = ISABELLE_GHC]
302    Code_Test_GHC
303  theories [condition = ISABELLE_MLTON]
304    Code_Test_MLton
305  theories [condition = ISABELLE_OCAMLFIND]
306    Code_Test_OCaml
307  theories [condition = ISABELLE_SMLNJ]
308    Code_Test_SMLNJ
309
310session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" +
311  description "
312    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
313    Author:     Jasmin Blanchette, TU Muenchen
314
315    Testing Metis and Sledgehammer.
316  "
317  sessions
318    "HOL-Decision_Procs"
319  theories
320    Abstraction
321    Big_O
322    Binary_Tree
323    Clausification
324    Message
325    Proxies
326    Tarski
327    Trans_Closure
328    Sets
329
330session "HOL-Nitpick_Examples" in Nitpick_Examples = "HOL-Library" +
331  description "
332    Author:     Jasmin Blanchette, TU Muenchen
333    Copyright   2009
334  "
335  theories [quick_and_dirty] Nitpick_Examples
336
337session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" +
338  description "
339    Author: Clemens Ballarin, started 24 September 1999, and many others
340
341    The Isabelle Algebraic Library.
342  "
343  sessions
344    "HOL-Cardinals"
345  theories
346    (* Orders and Lattices *)
347    Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
348    (* Groups *)
349    FiniteProduct        (* Product operator for commutative groups *)
350    Sylow                (* Sylow's theorem *)
351    Bij                  (* Automorphism Groups *)
352    Multiplicative_Group
353    Zassenhaus            (* The Zassenhaus lemma *)
354    (* Rings *)
355    Divisibility         (* Rings *)
356    IntRing              (* Ideals and residue classes *)
357    UnivPoly             (* Polynomials *)
358    (* Main theory *)
359    Algebra
360  document_files "root.bib" "root.tex"
361
362session "HOL-Auth" (timing) in Auth = "HOL-Library" +
363  description "
364    A new approach to verifying authentication protocols.
365  "
366  directories "Smartcard" "Guard"
367  theories
368    Auth_Shared
369    Auth_Public
370    "Smartcard/Auth_Smartcard"
371    "Guard/Auth_Guard_Shared"
372    "Guard/Auth_Guard_Public"
373  document_files "root.tex"
374
375session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" +
376  description "
377    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
378    Copyright   1998  University of Cambridge
379
380    Verifying security protocols using Chandy and Misra's UNITY formalism.
381  "
382  directories "Simple" "Comp"
383  theories
384    (*Basic meta-theory*)
385    UNITY_Main
386
387    (*Simple examples: no composition*)
388    "Simple/Deadlock"
389    "Simple/Common"
390    "Simple/Network"
391    "Simple/Token"
392    "Simple/Channel"
393    "Simple/Lift"
394    "Simple/Mutex"
395    "Simple/Reach"
396    "Simple/Reachability"
397
398    (*Verifying security protocols using UNITY*)
399    "Simple/NSP_Bad"
400
401    (*Example of composition*)
402    "Comp/Handshake"
403
404    (*Universal properties examples*)
405    "Comp/Counter"
406    "Comp/Counterc"
407    "Comp/Priority"
408
409    "Comp/TimerArray"
410    "Comp/Progress"
411
412    "Comp/Alloc"
413    "Comp/AllocImpl"
414    "Comp/Client"
415
416    (*obsolete*)
417    ELT
418  document_files "root.tex"
419
420session "HOL-Unix" in Unix = "HOL-Library" +
421  options [print_mode = "no_brackets,no_type_brackets"]
422  theories Unix
423  document_files "root.bib" "root.tex"
424
425session "HOL-ZF" in ZF = "HOL-Library" +
426  theories
427    MainZF
428    Games
429  document_files "root.tex"
430
431session "HOL-Imperative_HOL" (timing) in Imperative_HOL = "HOL-Library" +
432  options [print_mode = "iff,no_brackets"]
433  directories "ex"
434  theories Imperative_HOL_ex
435  document_files "root.bib" "root.tex"
436
437session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" +
438  description "
439    Various decision procedures, typically involving reflection.
440  "
441  directories "ex"
442  theories
443    Decision_Procs
444
445session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
446  sessions
447    "HOL-Isar_Examples"
448  theories
449    Hilbert_Classical
450    Proof_Terms
451    XML_Data
452
453session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" +
454  description "
455    Examples for program extraction in Higher-Order Logic.
456  "
457  options [quick_and_dirty = false]
458  sessions
459    "HOL-Computational_Algebra"
460  theories
461    Greatest_Common_Divisor
462    Warshall
463    Higman_Extraction
464    Pigeonhole
465    Euclid
466  document_files "root.bib" "root.tex"
467
468session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" +
469  description \<open>
470    Lambda Calculus in de Bruijn's Notation.
471
472    This session defines lambda-calculus terms with de Bruijn indixes and
473    proves confluence of beta, eta and beta+eta.
474
475    The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
476    theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
477  \<close>
478  options [print_mode = "no_brackets", quick_and_dirty = false]
479  sessions
480    "HOL-Library"
481  theories
482    Eta
483    StrongNorm
484    Standardization
485    WeakNorm
486  document_files "root.bib" "root.tex"
487
488session "HOL-Prolog" in Prolog = HOL +
489  description "
490    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
491
492    A bare-bones implementation of Lambda-Prolog.
493
494    This is a simple exploratory implementation of Lambda-Prolog in HOL,
495    including some minimal examples (in Test.thy) and a more typical example of
496    a little functional language and its type system.
497  "
498  theories Test Type
499
500session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" +
501  description "
502    Formalization of a fragment of Java, together with a corresponding virtual
503    machine and a specification of its bytecode verifier and a lightweight
504    bytecode verifier, including proofs of type-safety.
505  "
506  sessions
507    "HOL-Eisbach"
508  directories "BV" "Comp" "DFA" "J" "JVM"
509  theories
510    MicroJava
511  document_files
512    "introduction.tex"
513    "root.bib"
514    "root.tex"
515
516session "HOL-NanoJava" in NanoJava = HOL +
517  description "
518    Hoare Logic for a tiny fragment of Java.
519  "
520  theories Example
521  document_files "root.bib" "root.tex"
522
523session "HOL-Bali" (timing) in Bali = "HOL-Library" +
524  theories
525    AxExample
526    AxSound
527    AxCompl
528    Trans
529    TypeSafe
530  document_files "root.tex"
531
532session "HOL-IOA" in IOA = HOL +
533  description \<open>
534    Author:     Tobias Nipkow and Konrad Slind and Olaf M��ller
535    Copyright   1994--1996  TU Muenchen
536
537    The meta-theory of I/O-Automata in HOL. This formalization has been
538    significantly changed and extended, see HOLCF/IOA. There are also the
539    proofs of two communication protocols which formerly have been here.
540
541    @inproceedings{Nipkow-Slind-IOA,
542    author={Tobias Nipkow and Konrad Slind},
543    title={{I/O} Automata in {Isabelle/HOL}},
544    booktitle={Proc.\ TYPES Workshop 1994},
545    publisher=Springer,
546    series=LNCS,
547    note={To appear}}
548    ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
549
550    and
551
552    @inproceedings{Mueller-Nipkow,
553    author={Olaf M\"uller and Tobias Nipkow},
554    title={Combining Model Checking and Deduction for {I/O}-Automata},
555    booktitle={Proc.\ TACAS Workshop},
556    organization={Aarhus University, BRICS report},
557    year=1995}
558    ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
559  \<close>
560  theories Solve
561
562session "HOL-Lattice" in Lattice = HOL +
563  description "
564    Author:     Markus Wenzel, TU Muenchen
565
566    Basic theory of lattices and orders.
567  "
568  theories CompleteLattice
569  document_files "root.tex"
570
571session "HOL-ex" (timing) in ex = "HOL-Number_Theory" +
572  description "
573    Miscellaneous examples for Higher-Order Logic.
574  "
575  theories
576    Adhoc_Overloading_Examples
577    Antiquote
578    Argo_Examples
579    Arith_Examples
580    Ballot
581    BinEx
582    Birthday_Paradox
583    Bit_Lists
584    Bubblesort
585    CTL
586    Cartouche_Examples
587    Case_Product
588    Chinese
589    Classical
590    Code_Binary_Nat_examples
591    Code_Lazy_Demo
592    Code_Timing
593    Coercion_Examples
594    Coherent
595    Commands
596    Computations
597    Conditional_Parametricity_Examples
598    Cubic_Quartic
599    Datatype_Record_Examples
600    Dedekind_Real
601    Erdoes_Szekeres
602    Eval_Examples
603    Executable_Relation
604    Execute_Choice
605    Functions
606    Function_Growth
607    Gauge_Integration
608    Groebner_Examples
609    Guess
610    HarmonicSeries
611    Hebrew
612    Hex_Bin_Examples
613    IArray_Examples
614    Iff_Oracle
615    Induction_Schema
616    Intuitionistic
617    Join_Theory
618    Lagrange
619    List_to_Set_Comprehension_Examples
620    LocaleTest2
621    "ML"
622    MergeSort
623    MonoidGroup
624    Multiquote
625    NatSum
626    Normalization_by_Evaluation
627    PER
628    Parallel_Example
629    Peano_Axioms
630    Perm_Fragments
631    PresburgerEx
632    Primrec
633    Pythagoras
634    Quicksort
635    Radix_Sort
636    Records
637    Reflection_Examples
638    Refute_Examples
639    Residue_Ring
640    Rewrite_Examples
641    SOS
642    SOS_Cert
643    Seq
644    Serbian
645    Set_Comprehension_Pointfree_Examples
646    Set_Theory
647    Simproc_Tests
648    Simps_Case_Conv_Examples
649    Sketch_and_Explore
650    Sorting_Algorithms_Examples
651    Sqrt
652    Sqrt_Script
653    Sudoku
654    Sum_of_Powers
655    Tarski
656    Termination
657    ThreeDivides
658    Transfer_Debug
659    Transfer_Int_Nat
660    Transitive_Closure_Table_Ex
661    Tree23
662    Triangular_Numbers
663    Unification
664    While_Combinator_Example
665    Word
666    veriT_Preprocessing
667  theories [skip_proofs = false]
668    SAT_Examples
669    Meson_Test
670
671session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" +
672  description "
673    Miscellaneous Isabelle/Isar examples.
674  "
675  options [quick_and_dirty]
676  theories
677    Knaster_Tarski
678    Peirce
679    Drinker
680    Cantor
681    Structured_Statements
682    Basic_Logic
683    Expr_Compiler
684    Fibonacci
685    Group
686    Group_Context
687    Group_Notepad
688    Hoare_Ex
689    Mutilated_Checkerboard
690    Puzzle
691    Summation
692    First_Order_Logic
693    Higher_Order_Logic
694  document_files
695    "root.bib"
696    "root.tex"
697
698session "HOL-Eisbach" in Eisbach = HOL +
699  description \<open>
700    The Eisbach proof method language and "match" method.
701  \<close>
702  sessions
703    FOL
704    "HOL-Analysis"
705  theories
706    Eisbach
707    Tests
708    Examples
709    Examples_FOL
710    Example_Metric
711
712session "HOL-SET_Protocol" (timing) in SET_Protocol = "HOL-Library" +
713  description "
714    Verification of the SET Protocol.
715  "
716  theories
717    SET_Protocol
718  document_files "root.tex"
719
720session "HOL-Matrix_LP" in Matrix_LP = "HOL-Library" +
721  description "
722    Two-dimensional matrices and linear programming.
723  "
724  directories "Compute_Oracle"
725  theories Cplex
726  document_files "root.tex"
727
728session "HOL-TLA" in TLA = HOL +
729  description "
730    Lamport's Temporal Logic of Actions.
731  "
732  theories TLA
733
734session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
735  theories Inc
736
737session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
738  theories DBuffer
739
740session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
741  theories MemoryImplementation
742
743session "HOL-TPTP" in TPTP = "HOL-Library" +
744  description "
745    Author:     Jasmin Blanchette, TU Muenchen
746    Author:     Nik Sultana, University of Cambridge
747    Copyright   2011
748
749    TPTP-related extensions.
750  "
751  theories
752    ATP_Theory_Export
753    MaSh_Eval
754    TPTP_Interpret
755    THF_Arith
756    TPTP_Proof_Reconstruction
757  theories
758    ATP_Problem_Import
759
760session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
761  theories
762    Probability
763  document_files "root.tex"
764
765session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
766  theories
767    Dining_Cryptographers
768    Koepf_Duermuth_Countermeasure
769    Measure_Not_CCC
770
771session "HOL-Nominal" in Nominal = "HOL-Library" +
772  theories
773    Nominal
774
775session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" +
776  theories
777    Class3
778    CK_Machine
779    Compile
780    Contexts
781    Crary
782    CR_Takahashi
783    CR
784    Fsub
785    Height
786    Lambda_mu
787    Lam_Funs
788    LocalWeakening
789    Pattern
790    SN
791    SOS
792    Standardization
793    Support
794    Type_Preservation
795    Weakening
796    W
797  theories [quick_and_dirty]
798    VC_Condition
799
800session "HOL-Cardinals" (timing) in Cardinals = HOL +
801  description "
802    Ordinals and Cardinals, Full Theories.
803  "
804  theories
805    Cardinals
806    Bounded_Set
807  document_files
808    "intro.tex"
809    "root.tex"
810    "root.bib"
811
812session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" +
813  description "
814    (Co)datatype Examples.
815  "
816  directories "Derivation_Trees"
817  theories
818    Compat
819    Lambda_Term
820    Process
821    TreeFsetI
822    "Derivation_Trees/Gram_Lang"
823    "Derivation_Trees/Parallel_Composition"
824    Koenig
825    Lift_BNF
826    Milner_Tofte
827    Stream_Processor
828    Cyclic_List
829    Free_Idempotent_Monoid
830    LDL
831    TLList
832    Misc_Codatatype
833    Misc_Datatype
834    Misc_Primcorec
835    Misc_Primrec
836
837session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" +
838  description "
839    Corecursion Examples.
840  "
841  directories "Tests"
842  theories
843    LFilter
844    Paper_Examples
845    Stream_Processor
846    "Tests/Simple_Nesting"
847    "Tests/Iterate_GPV"
848  theories [quick_and_dirty]
849    "Tests/GPV_Bare_Bones"
850    "Tests/Merge_D"
851    "Tests/Merge_Poly"
852    "Tests/Misc_Mono"
853    "Tests/Misc_Poly"
854    "Tests/Small_Concrete"
855    "Tests/Stream_Friends"
856    "Tests/TLList_Friends"
857    "Tests/Type_Class"
858
859session "HOL-Word" (main timing) in Word = HOL +
860  sessions
861    "HOL-Library"
862  theories
863    Word
864    More_Word
865    Word_Examples
866  document_files "root.bib" "root.tex"
867
868session "HOL-Statespace" in Statespace = HOL +
869  theories [skip_proofs = false]
870    StateSpaceEx
871  document_files "root.tex"
872
873session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" +
874  description "
875    Nonstandard analysis.
876  "
877  theories
878    Nonstandard_Analysis
879  document_files "root.tex"
880
881session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
882  theories
883    NSPrimes
884
885session "HOL-Mirabelle" in Mirabelle = HOL +
886  theories Mirabelle_Test
887
888session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
889  options [timeout = 60]
890  theories Ex
891
892session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" +
893  options [quick_and_dirty]
894  theories
895    Boogie
896    SMT_Examples
897    SMT_Word_Examples
898    SMT_Tests
899
900session "HOL-SPARK" in "SPARK" = "HOL-Word" +
901  theories
902    SPARK
903
904session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
905  directories "Gcd" "Liseq" "RIPEMD-160" "Sqrt"
906  theories
907    "Gcd/Greatest_Common_Divisor"
908    "Liseq/Longest_Increasing_Subsequence"
909    "RIPEMD-160/F"
910    "RIPEMD-160/Hash"
911    "RIPEMD-160/K_L"
912    "RIPEMD-160/K_R"
913    "RIPEMD-160/R_L"
914    "RIPEMD-160/Round"
915    "RIPEMD-160/R_R"
916    "RIPEMD-160/S_L"
917    "RIPEMD-160/S_R"
918    "Sqrt/Sqrt"
919  export_files (in ".") "*:**.prv"
920
921session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
922  options [show_question_marks = false]
923  sessions
924    "HOL-SPARK-Examples"
925  theories
926    Example_Verification
927    VC_Principles
928    Reference
929    Complex_Types
930  document_files
931    "complex_types.ads"
932    "complex_types_app.adb"
933    "complex_types_app.ads"
934    "Gcd.adb"
935    "Gcd.ads"
936    "intro.tex"
937    "loop_invariant.adb"
938    "loop_invariant.ads"
939    "root.bib"
940    "root.tex"
941    "Simple_Gcd.adb"
942    "Simple_Gcd.ads"
943
944session "HOL-Mutabelle" in Mutabelle = "HOL-Library" +
945  theories MutabelleExtra
946
947session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = "HOL-Library" +
948  theories
949    Quickcheck_Examples
950    Quickcheck_Lattice_Examples
951    Completeness
952    Quickcheck_Interfaces
953    Quickcheck_Nesting_Example
954  theories [condition = ISABELLE_GHC]
955    Hotel_Example
956    Quickcheck_Narrowing_Examples
957
958session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" +
959  description "
960    Author:     Cezary Kaliszyk and Christian Urban
961  "
962  theories
963    DList
964    Quotient_FSet
965    Quotient_Int
966    Quotient_Message
967    Lift_FSet
968    Lift_Set
969    Lift_Fun
970    Quotient_Rat
971    Lift_DList
972    Int_Pow
973    Lifting_Code_Dt_Test
974
975session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = "HOL-Library" +
976  theories
977    Examples
978    Predicate_Compile_Tests
979    Predicate_Compile_Quickcheck_Examples
980    Specialisation_Examples
981    IMP_1
982    IMP_2
983    (* FIXME since 21-Jul-2011
984    Hotel_Example_Small_Generator *)
985    IMP_3
986    IMP_4
987  theories [condition = ISABELLE_SWIPL]
988    Code_Prolog_Examples
989    Context_Free_Grammar_Example
990    Hotel_Example_Prolog
991    Lambda_Example
992    List_Examples
993  theories [condition = ISABELLE_SWIPL, quick_and_dirty]
994    Reg_Exp_Example
995
996session "HOL-Types_To_Sets" in Types_To_Sets = HOL +
997  description "
998    Experimental extension of Higher-Order Logic to allow translation of types to sets.
999  "
1000  directories "Examples"
1001  theories
1002    Types_To_Sets
1003    "Examples/Prerequisites"
1004    "Examples/Finite"
1005    "Examples/T2_Spaces"
1006    "Examples/Unoverload_Def"
1007    "Examples/Linear_Algebra_On"
1008
1009session HOLCF (main timing) in HOLCF = HOL +
1010  description "
1011    Author:     Franz Regensburger
1012    Author:     Brian Huffman
1013
1014    HOLCF -- a semantic extension of HOL by the LCF logic.
1015  "
1016  sessions
1017    "HOL-Library"
1018  theories
1019    HOLCF (global)
1020  document_files "root.tex"
1021
1022session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
1023  theories
1024    Domain_ex
1025    Fixrec_ex
1026    New_Domain
1027  document_files "root.tex"
1028
1029session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
1030  theories
1031    HOLCF_Library
1032    HOL_Cpo
1033
1034session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
1035  description "
1036    IMP -- A WHILE-language and its Semantics.
1037
1038    This is the HOLCF-based denotational semantics of a simple WHILE-language.
1039  "
1040  sessions
1041    "HOL-IMP"
1042  theories
1043    HoareEx
1044  document_files
1045    "isaverbatimwrite.sty"
1046    "root.tex"
1047    "root.bib"
1048
1049session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" +
1050  description "
1051    Miscellaneous examples for HOLCF.
1052  "
1053  theories
1054    Dnat
1055    Dagstuhl
1056    Focus_ex
1057    Fix2
1058    Hoare
1059    Concurrency_Monad
1060    Loop
1061    Powerdomain_ex
1062    Domain_Proofs
1063    Letrec
1064    Pattern_Match
1065
1066session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" +
1067  description \<open>
1068    FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
1069
1070    For introductions to FOCUS, see
1071
1072    "The Design of Distributed Systems - An Introduction to FOCUS"
1073    http://www4.in.tum.de/publ/html.php?e=2
1074
1075    "Specification and Refinement of a Buffer of Length One"
1076    http://www4.in.tum.de/publ/html.php?e=15
1077
1078    "Specification and Development of Interactive Systems: Focus on Streams,
1079    Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
1080  \<close>
1081  theories
1082    Fstreams
1083    FOCUS
1084    Buffer_adm
1085
1086session IOA (timing) in "HOLCF/IOA" = HOLCF +
1087  description "
1088    Author:     Olaf Mueller
1089    Copyright   1997 TU M��nchen
1090
1091    A formalization of I/O automata in HOLCF.
1092
1093    The distribution contains simulation relations, temporal logic, and an
1094    abstraction theory. Everything is based upon a domain-theoretic model of
1095    finite and infinite sequences.
1096  "
1097  theories Abstraction
1098
1099session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
1100  description "
1101    Author:     Olaf Mueller
1102
1103    The Alternating Bit Protocol performed in I/O-Automata.
1104  "
1105  theories
1106    Correctness
1107    Spec
1108
1109session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
1110  description "
1111    Author:     Tobias Nipkow & Konrad Slind
1112
1113    A network transmission protocol, performed in the
1114    I/O automata formalization by Olaf Mueller.
1115  "
1116  theories Correctness
1117
1118session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
1119  description "
1120    Author:     Olaf Mueller
1121
1122    Memory storage case study.
1123  "
1124  theories Correctness
1125
1126session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
1127  description "
1128    Author:     Olaf Mueller
1129  "
1130  theories
1131    TrivEx
1132    TrivEx2
1133