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