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