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