src/HOL/ROOT
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (19 months ago)
changeset 67022 49309fe530fd
parent 67019 7a3724078363
child 67100 c7694d51c278
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     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 [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     VCG_Total_EX2
   157     Collecting1
   158     Collecting_Examples
   159     Abs_Int_Tests
   160     Abs_Int1_parity
   161     Abs_Int1_const
   162     Abs_Int3
   163     Procs_Dyn_Vars_Dyn
   164     Procs_Stat_Vars_Dyn
   165     Procs_Stat_Vars_Stat
   166     C_like
   167     OO
   168   document_files "root.bib" "root.tex"
   169 
   170 session "HOL-IMPP" in IMPP = HOL +
   171   description {*
   172     Author:     David von Oheimb
   173     Copyright   1999 TUM
   174 
   175     IMPP -- An imperative language with procedures.
   176 
   177     This is an extension of IMP with local variables and mutually recursive
   178     procedures. For documentation see "Hoare Logic for Mutual Recursion and
   179     Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
   180   *}
   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   sessions
   237     "HOL-Data_Structures"
   238     "HOL-ex"
   239   theories
   240     Generate
   241     Generate_Binary_Nat
   242     Generate_Target_Nat
   243     Generate_Efficient_Datastructures
   244     Generate_Pretty_Char
   245     Code_Test_PolyML
   246     Code_Test_Scala
   247   theories [condition = ISABELLE_GHC]
   248     Code_Test_GHC
   249   theories [condition = ISABELLE_MLTON]
   250     Code_Test_MLton
   251   theories [condition = ISABELLE_OCAMLC]
   252     Code_Test_OCaml
   253   theories [condition = ISABELLE_SMLNJ]
   254     Code_Test_SMLNJ
   255 
   256 session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" +
   257   description {*
   258     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   259     Author:     Jasmin Blanchette, TU Muenchen
   260 
   261     Testing Metis and Sledgehammer.
   262   *}
   263   sessions
   264     "HOL-Decision_Procs"
   265   theories
   266     Abstraction
   267     Big_O
   268     Binary_Tree
   269     Clausification
   270     Message
   271     Proxies
   272     Tarski
   273     Trans_Closure
   274     Sets
   275 
   276 session "HOL-Nitpick_Examples" in Nitpick_Examples = "HOL-Library" +
   277   description {*
   278     Author:     Jasmin Blanchette, TU Muenchen
   279     Copyright   2009
   280   *}
   281   theories [quick_and_dirty] Nitpick_Examples
   282 
   283 session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" +
   284   description {*
   285     Author: Clemens Ballarin, started 24 September 1999
   286 
   287     The Isabelle Algebraic Library.
   288   *}
   289   theories
   290     (* Orders and Lattices *)
   291     Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
   292 
   293     (* Groups *)
   294     FiniteProduct        (* Product operator for commutative groups *)
   295     Sylow                (* Sylow's theorem *)
   296     Bij                  (* Automorphism Groups *)
   297     More_Group
   298     More_Finite_Product
   299     Multiplicative_Group
   300 
   301     (* Rings *)
   302     Divisibility         (* Rings *)
   303     IntRing              (* Ideals and residue classes *)
   304     UnivPoly             (* Polynomials *)
   305     More_Ring
   306   document_files "root.bib" "root.tex"
   307 
   308 session "HOL-Auth" (timing) in Auth = "HOL-Library" +
   309   description {*
   310     A new approach to verifying authentication protocols.
   311   *}
   312   theories
   313     Auth_Shared
   314     Auth_Public
   315     "Smartcard/Auth_Smartcard"
   316     "Guard/Auth_Guard_Shared"
   317     "Guard/Auth_Guard_Public"
   318   document_files "root.tex"
   319 
   320 session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" +
   321   description {*
   322     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   323     Copyright   1998  University of Cambridge
   324 
   325     Verifying security protocols using Chandy and Misra's UNITY formalism.
   326   *}
   327   theories
   328     (*Basic meta-theory*)
   329     UNITY_Main
   330 
   331     (*Simple examples: no composition*)
   332     "Simple/Deadlock"
   333     "Simple/Common"
   334     "Simple/Network"
   335     "Simple/Token"
   336     "Simple/Channel"
   337     "Simple/Lift"
   338     "Simple/Mutex"
   339     "Simple/Reach"
   340     "Simple/Reachability"
   341 
   342     (*Verifying security protocols using UNITY*)
   343     "Simple/NSP_Bad"
   344 
   345     (*Example of composition*)
   346     "Comp/Handshake"
   347 
   348     (*Universal properties examples*)
   349     "Comp/Counter"
   350     "Comp/Counterc"
   351     "Comp/Priority"
   352 
   353     "Comp/TimerArray"
   354     "Comp/Progress"
   355 
   356     "Comp/Alloc"
   357     "Comp/AllocImpl"
   358     "Comp/Client"
   359 
   360     (*obsolete*)
   361     ELT
   362   document_files "root.tex"
   363 
   364 session "HOL-Unix" in Unix = "HOL-Library" +
   365   options [print_mode = "no_brackets,no_type_brackets"]
   366   theories Unix
   367   document_files "root.bib" "root.tex"
   368 
   369 session "HOL-ZF" in ZF = "HOL-Library" +
   370   theories
   371     MainZF
   372     Games
   373   document_files "root.tex"
   374 
   375 session "HOL-Imperative_HOL" (timing) in Imperative_HOL = "HOL-Library" +
   376   options [print_mode = "iff,no_brackets"]
   377   theories Imperative_HOL_ex
   378   document_files "root.bib" "root.tex"
   379 
   380 session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" +
   381   description {*
   382     Various decision procedures, typically involving reflection.
   383   *}
   384   theories
   385     Decision_Procs
   386 
   387 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
   388   sessions
   389     "HOL-Isar_Examples"
   390   theories
   391     Hilbert_Classical
   392     Proof_Terms
   393     XML_Data
   394 
   395 session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" +
   396   description {*
   397     Examples for program extraction in Higher-Order Logic.
   398   *}
   399   options [parallel_proofs = 0, quick_and_dirty = false]
   400   sessions
   401     "HOL-Computational_Algebra"
   402   theories
   403     Greatest_Common_Divisor
   404     Warshall
   405     Higman_Extraction
   406     Pigeonhole
   407     Euclid
   408   document_files "root.bib" "root.tex"
   409 
   410 session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" +
   411   description {*
   412     Lambda Calculus in de Bruijn's Notation.
   413 
   414     This session defines lambda-calculus terms with de Bruijn indixes and
   415     proves confluence of beta, eta and beta+eta.
   416 
   417     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
   418     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
   419   *}
   420   options [print_mode = "no_brackets",
   421     parallel_proofs = 0, quick_and_dirty = false]
   422   sessions
   423     "HOL-Library"
   424   theories
   425     Eta
   426     StrongNorm
   427     Standardization
   428     WeakNorm
   429   document_files "root.bib" "root.tex"
   430 
   431 session "HOL-Prolog" in Prolog = HOL +
   432   description {*
   433     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
   434 
   435     A bare-bones implementation of Lambda-Prolog.
   436 
   437     This is a simple exploratory implementation of Lambda-Prolog in HOL,
   438     including some minimal examples (in Test.thy) and a more typical example of
   439     a little functional language and its type system.
   440   *}
   441   theories Test Type
   442 
   443 session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" +
   444   description {*
   445     Formalization of a fragment of Java, together with a corresponding virtual
   446     machine and a specification of its bytecode verifier and a lightweight
   447     bytecode verifier, including proofs of type-safety.
   448   *}
   449   sessions
   450     "HOL-Eisbach"
   451   theories
   452     MicroJava
   453   document_files
   454     "introduction.tex"
   455     "root.bib"
   456     "root.tex"
   457 
   458 session "HOL-NanoJava" in NanoJava = HOL +
   459   description {*
   460     Hoare Logic for a tiny fragment of Java.
   461   *}
   462   theories Example
   463   document_files "root.bib" "root.tex"
   464 
   465 session "HOL-Bali" (timing) in Bali = "HOL-Library" +
   466   theories
   467     AxExample
   468     AxSound
   469     AxCompl
   470     Trans
   471     TypeSafe
   472   document_files "root.tex"
   473 
   474 session "HOL-IOA" in IOA = HOL +
   475   description {*
   476     Author:     Tobias Nipkow and Konrad Slind and Olaf Müller
   477     Copyright   1994--1996  TU Muenchen
   478 
   479     The meta-theory of I/O-Automata in HOL. This formalization has been
   480     significantly changed and extended, see HOLCF/IOA. There are also the
   481     proofs of two communication protocols which formerly have been here.
   482 
   483     @inproceedings{Nipkow-Slind-IOA,
   484     author={Tobias Nipkow and Konrad Slind},
   485     title={{I/O} Automata in {Isabelle/HOL}},
   486     booktitle={Proc.\ TYPES Workshop 1994},
   487     publisher=Springer,
   488     series=LNCS,
   489     note={To appear}}
   490     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
   491 
   492     and
   493 
   494     @inproceedings{Mueller-Nipkow,
   495     author={Olaf M\"uller and Tobias Nipkow},
   496     title={Combining Model Checking and Deduction for {I/O}-Automata},
   497     booktitle={Proc.\ TACAS Workshop},
   498     organization={Aarhus University, BRICS report},
   499     year=1995}
   500     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
   501   *}
   502   theories Solve
   503 
   504 session "HOL-Lattice" in Lattice = HOL +
   505   description {*
   506     Author:     Markus Wenzel, TU Muenchen
   507 
   508     Basic theory of lattices and orders.
   509   *}
   510   theories CompleteLattice
   511   document_files "root.tex"
   512 
   513 session "HOL-ex" (timing) in ex = "HOL-Number_Theory" +
   514   description {*
   515     Miscellaneous examples for Higher-Order Logic.
   516   *}
   517   theories
   518     Adhoc_Overloading_Examples
   519     Antiquote
   520     Argo_Examples
   521     Arith_Examples
   522     Ballot
   523     BinEx
   524     Birthday_Paradox
   525     Bubblesort
   526     CTL
   527     Cartouche_Examples
   528     Case_Product
   529     Chinese
   530     Classical
   531     Code_Binary_Nat_examples
   532     Code_Timing
   533     Coercion_Examples
   534     Coherent
   535     Commands
   536     Computations
   537     Cubic_Quartic
   538     Dedekind_Real
   539     Erdoes_Szekeres
   540     Eval_Examples
   541     Executable_Relation
   542     Execute_Choice
   543     Functions
   544     Function_Growth
   545     Gauge_Integration
   546     Groebner_Examples
   547     Guess
   548     HarmonicSeries
   549     Hebrew
   550     Hex_Bin_Examples
   551     IArray_Examples
   552     Iff_Oracle
   553     Induction_Schema
   554     Intuitionistic
   555     Lagrange
   556     List_to_Set_Comprehension_Examples
   557     LocaleTest2
   558     ML
   559     MergeSort
   560     MonoidGroup
   561     Multiquote
   562     NatSum
   563     Normalization_by_Evaluation
   564     PER
   565     Parallel_Example
   566     Peano_Axioms
   567     Perm_Fragments
   568     PresburgerEx
   569     Primrec
   570     Pythagoras
   571     Quicksort
   572     Records
   573     Reflection_Examples
   574     Refute_Examples
   575     Rewrite_Examples
   576     SAT_Examples
   577     SOS
   578     SOS_Cert
   579     Seq
   580     Serbian
   581     Set_Comprehension_Pointfree_Examples
   582     Set_Theory
   583     Simproc_Tests
   584     Simps_Case_Conv_Examples
   585     Sqrt
   586     Sqrt_Script
   587     Sudoku
   588     Sum_of_Powers
   589     Tarski
   590     Termination
   591     ThreeDivides
   592     Transfer_Debug
   593     Transfer_Int_Nat
   594     Transitive_Closure_Table_Ex
   595     Tree23
   596     Unification
   597     While_Combinator_Example
   598     Word_Type
   599     veriT_Preprocessing
   600   theories [skip_proofs = false]
   601     Meson_Test
   602 
   603 session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" +
   604   description {*
   605     Miscellaneous Isabelle/Isar examples.
   606   *}
   607   options [quick_and_dirty]
   608   theories
   609     Knaster_Tarski
   610     Peirce
   611     Drinker
   612     Cantor
   613     Structured_Statements
   614     Basic_Logic
   615     Expr_Compiler
   616     Fibonacci
   617     Group
   618     Group_Context
   619     Group_Notepad
   620     Hoare_Ex
   621     Mutilated_Checkerboard
   622     Puzzle
   623     Summation
   624     First_Order_Logic
   625     Higher_Order_Logic
   626   document_files
   627     "root.bib"
   628     "root.tex"
   629 
   630 session "HOL-Eisbach" in Eisbach = HOL +
   631   description {*
   632     The Eisbach proof method language and "match" method.
   633   *}
   634   sessions
   635     FOL
   636   theories
   637     Eisbach
   638     Tests
   639     Examples
   640     Examples_FOL
   641 
   642 session "HOL-SET_Protocol" (timing) in SET_Protocol = "HOL-Library" +
   643   description {*
   644     Verification of the SET Protocol.
   645   *}
   646   theories
   647     SET_Protocol
   648   document_files "root.tex"
   649 
   650 session "HOL-Matrix_LP" in Matrix_LP = "HOL-Library" +
   651   description {*
   652     Two-dimensional matrices and linear programming.
   653   *}
   654   theories Cplex
   655   document_files "root.tex"
   656 
   657 session "HOL-TLA" in TLA = HOL +
   658   description {*
   659     Lamport's Temporal Logic of Actions.
   660   *}
   661   theories TLA
   662 
   663 session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
   664   theories Inc
   665 
   666 session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
   667   theories DBuffer
   668 
   669 session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
   670   theories MemoryImplementation
   671 
   672 session "HOL-TPTP" in TPTP = "HOL-Library" +
   673   description {*
   674     Author:     Jasmin Blanchette, TU Muenchen
   675     Author:     Nik Sultana, University of Cambridge
   676     Copyright   2011
   677 
   678     TPTP-related extensions.
   679   *}
   680   theories
   681     ATP_Theory_Export
   682     MaSh_Eval
   683     TPTP_Interpret
   684     THF_Arith
   685     TPTP_Proof_Reconstruction
   686   theories
   687     ATP_Problem_Import
   688 
   689 session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
   690   theories
   691     Probability
   692   document_files "root.tex"
   693 
   694 session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
   695   theories
   696     Dining_Cryptographers
   697     Koepf_Duermuth_Countermeasure
   698     Measure_Not_CCC
   699 
   700 session "HOL-Nominal" in Nominal = "HOL-Library" +
   701   theories
   702     Nominal
   703 
   704 session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" +
   705   theories
   706     Class3
   707     CK_Machine
   708     Compile
   709     Contexts
   710     Crary
   711     CR_Takahashi
   712     CR
   713     Fsub
   714     Height
   715     Lambda_mu
   716     Lam_Funs
   717     LocalWeakening
   718     Pattern
   719     SN
   720     SOS
   721     Standardization
   722     Support
   723     Type_Preservation
   724     Weakening
   725     W
   726   theories [quick_and_dirty]
   727     VC_Condition
   728 
   729 session "HOL-Cardinals" (timing) in Cardinals = "HOL-Library" +
   730   description {*
   731     Ordinals and Cardinals, Full Theories.
   732   *}
   733   theories
   734     Cardinals
   735     Bounded_Set
   736   document_files
   737     "intro.tex"
   738     "root.tex"
   739     "root.bib"
   740 
   741 session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" +
   742   description {*
   743     (Co)datatype Examples.
   744   *}
   745   theories
   746     Compat
   747     Lambda_Term
   748     Process
   749     TreeFsetI
   750     "Derivation_Trees/Gram_Lang"
   751     "Derivation_Trees/Parallel_Composition"
   752     Koenig
   753     Lift_BNF
   754     Milner_Tofte
   755     Stream_Processor
   756     Misc_Codatatype
   757     Misc_Datatype
   758     Misc_Primcorec
   759     Misc_Primrec
   760 
   761 session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" +
   762   description {*
   763     Corecursion Examples.
   764   *}
   765   theories
   766     LFilter
   767     Paper_Examples
   768     Stream_Processor
   769     "Tests/Simple_Nesting"
   770     "Tests/Iterate_GPV"
   771   theories [quick_and_dirty]
   772     "Tests/GPV_Bare_Bones"
   773     "Tests/Merge_D"
   774     "Tests/Merge_Poly"
   775     "Tests/Misc_Mono"
   776     "Tests/Misc_Poly"
   777     "Tests/Small_Concrete"
   778     "Tests/Stream_Friends"
   779     "Tests/TLList_Friends"
   780     "Tests/Type_Class"
   781 
   782 session "HOL-Word" (main timing) in Word = HOL +
   783   sessions
   784     "HOL-Library"
   785   theories
   786     Word
   787     WordBitwise
   788     Bit_Comparison
   789   document_files "root.bib" "root.tex"
   790 
   791 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   792   theories WordExamples
   793 
   794 session "HOL-Statespace" in Statespace = HOL +
   795   theories [skip_proofs = false]
   796     StateSpaceEx
   797   document_files "root.tex"
   798 
   799 session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" +
   800   description {*
   801     Nonstandard analysis.
   802   *}
   803   theories
   804     Nonstandard_Analysis
   805   document_files "root.tex"
   806 
   807 session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
   808   theories
   809     NSPrimes
   810 
   811 session "HOL-Mirabelle" in Mirabelle = HOL +
   812   theories Mirabelle_Test
   813 
   814 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   815   options [timeout = 60]
   816   theories Ex
   817 
   818 session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" +
   819   options [quick_and_dirty]
   820   theories
   821     Boogie
   822     SMT_Examples
   823     SMT_Word_Examples
   824     SMT_Tests
   825 
   826 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   827   theories
   828     SPARK
   829 
   830 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   831   options [spark_prv = false]
   832   theories
   833     "Gcd/Greatest_Common_Divisor"
   834     "Liseq/Longest_Increasing_Subsequence"
   835     "RIPEMD-160/F"
   836     "RIPEMD-160/Hash"
   837     "RIPEMD-160/K_L"
   838     "RIPEMD-160/K_R"
   839     "RIPEMD-160/R_L"
   840     "RIPEMD-160/Round"
   841     "RIPEMD-160/R_R"
   842     "RIPEMD-160/S_L"
   843     "RIPEMD-160/S_R"
   844     "Sqrt/Sqrt"
   845 
   846 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   847   options [show_question_marks = false, spark_prv = false]
   848   sessions
   849     "HOL-SPARK-Examples"
   850   theories
   851     Example_Verification
   852     VC_Principles
   853     Reference
   854     Complex_Types
   855   document_files
   856     "complex_types.ads"
   857     "complex_types_app.adb"
   858     "complex_types_app.ads"
   859     "Gcd.adb"
   860     "Gcd.ads"
   861     "intro.tex"
   862     "loop_invariant.adb"
   863     "loop_invariant.ads"
   864     "root.bib"
   865     "root.tex"
   866     "Simple_Gcd.adb"
   867     "Simple_Gcd.ads"
   868 
   869 session "HOL-Mutabelle" in Mutabelle = "HOL-Library" +
   870   theories MutabelleExtra
   871 
   872 session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = "HOL-Library" +
   873   theories
   874     Quickcheck_Examples
   875     Quickcheck_Lattice_Examples
   876     Completeness
   877     Quickcheck_Interfaces
   878     Quickcheck_Nesting_Example
   879   theories [condition = ISABELLE_GHC]
   880     Hotel_Example
   881     Quickcheck_Narrowing_Examples
   882 
   883 session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" +
   884   description {*
   885     Author:     Cezary Kaliszyk and Christian Urban
   886   *}
   887   theories
   888     DList
   889     Quotient_FSet
   890     Quotient_Int
   891     Quotient_Message
   892     Lift_FSet
   893     Lift_Set
   894     Lift_Fun
   895     Quotient_Rat
   896     Lift_DList
   897     Int_Pow
   898     Lifting_Code_Dt_Test
   899 
   900 session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = "HOL-Library" +
   901   theories
   902     Examples
   903     Predicate_Compile_Tests
   904     Predicate_Compile_Quickcheck_Examples
   905     Specialisation_Examples
   906     IMP_1
   907     IMP_2
   908     (* FIXME since 21-Jul-2011
   909     Hotel_Example_Small_Generator *)
   910     IMP_3
   911     IMP_4
   912   theories [condition = ISABELLE_SWIPL]
   913     Code_Prolog_Examples
   914     Context_Free_Grammar_Example
   915     Hotel_Example_Prolog
   916     Lambda_Example
   917     List_Examples
   918   theories [condition = ISABELLE_SWIPL, quick_and_dirty]
   919     Reg_Exp_Example
   920 
   921 session "HOL-Types_To_Sets" in Types_To_Sets = HOL +
   922   description {*
   923     Experimental extension of Higher-Order Logic to allow translation of types to sets.
   924   *}
   925   theories
   926     Types_To_Sets
   927     "Examples/Prerequisites"
   928     "Examples/Finite"
   929     "Examples/T2_Spaces"
   930 
   931 session HOLCF (main timing) in HOLCF = HOL +
   932   description {*
   933     Author:     Franz Regensburger
   934     Author:     Brian Huffman
   935 
   936     HOLCF -- a semantic extension of HOL by the LCF logic.
   937   *}
   938   sessions
   939     "HOL-Library"
   940   theories
   941     HOLCF (global)
   942   document_files "root.tex"
   943 
   944 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   945   theories
   946     Domain_ex
   947     Fixrec_ex
   948     New_Domain
   949   document_files "root.tex"
   950 
   951 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   952   theories
   953     HOLCF_Library
   954     HOL_Cpo
   955 
   956 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   957   description {*
   958     IMP -- A WHILE-language and its Semantics.
   959 
   960     This is the HOLCF-based denotational semantics of a simple WHILE-language.
   961   *}
   962   sessions
   963     "HOL-IMP"
   964   theories
   965     HoareEx
   966   document_files
   967     "isaverbatimwrite.sty"
   968     "root.tex"
   969     "root.bib"
   970 
   971 session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" +
   972   description {*
   973     Miscellaneous examples for HOLCF.
   974   *}
   975   theories
   976     Dnat
   977     Dagstuhl
   978     Focus_ex
   979     Fix2
   980     Hoare
   981     Concurrency_Monad
   982     Loop
   983     Powerdomain_ex
   984     Domain_Proofs
   985     Letrec
   986     Pattern_Match
   987 
   988 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" +
   989   description {*
   990     FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
   991 
   992     For introductions to FOCUS, see
   993 
   994     "The Design of Distributed Systems - An Introduction to FOCUS"
   995     http://www4.in.tum.de/publ/html.php?e=2
   996 
   997     "Specification and Refinement of a Buffer of Length One"
   998     http://www4.in.tum.de/publ/html.php?e=15
   999 
  1000     "Specification and Development of Interactive Systems: Focus on Streams,
  1001     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
  1002   *}
  1003   theories
  1004     Fstreams
  1005     FOCUS
  1006     Buffer_adm
  1007 
  1008 session IOA (timing) in "HOLCF/IOA" = HOLCF +
  1009   description {*
  1010     Author:     Olaf Mueller
  1011     Copyright   1997 TU München
  1012 
  1013     A formalization of I/O automata in HOLCF.
  1014 
  1015     The distribution contains simulation relations, temporal logic, and an
  1016     abstraction theory. Everything is based upon a domain-theoretic model of
  1017     finite and infinite sequences.
  1018   *}
  1019   theories Abstraction
  1020 
  1021 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  1022   description {*
  1023     Author:     Olaf Mueller
  1024 
  1025     The Alternating Bit Protocol performed in I/O-Automata.
  1026   *}
  1027   theories
  1028     Correctness
  1029     Spec
  1030 
  1031 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
  1032   description {*
  1033     Author:     Tobias Nipkow & Konrad Slind
  1034 
  1035     A network transmission protocol, performed in the
  1036     I/O automata formalization by Olaf Mueller.
  1037   *}
  1038   theories Correctness
  1039 
  1040 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
  1041   description {*
  1042     Author:     Olaf Mueller
  1043 
  1044     Memory storage case study.
  1045   *}
  1046   theories Correctness
  1047 
  1048 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
  1049   description {*
  1050     Author:     Olaf Mueller
  1051   *}
  1052   theories
  1053     TrivEx
  1054     TrivEx2