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