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