src/HOL/ROOT
author wenzelm
Wed Mar 13 17:13:22 2013 +0100 (2013-03-13)
changeset 51421 b5d559b101d9
parent 51403 2ff3a5589b05
child 51422 821a70e29e0b
permissions -rw-r--r--
more uniform session descriptions, which show up in chapter index;
     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]
    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 Generate Generate_Binary_Nat Generate_Target_Nat Generate_Efficient_Datastructures Generate_Pretty_Char
   214 
   215 session "HOL-Metis_Examples" in Metis_Examples = HOL +
   216   description {*
   217     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   218     Author:     Jasmin Blanchette, TU Muenchen
   219 
   220     Testing Metis and Sledgehammer.
   221   *}
   222   options [timeout = 3600, document = false]
   223   theories
   224     Abstraction
   225     Big_O
   226     Binary_Tree
   227     Clausification
   228     Message
   229     Proxies
   230     Tarski
   231     Trans_Closure
   232     Sets
   233 
   234 session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL +
   235   description {*
   236     Author:     Jasmin Blanchette, TU Muenchen
   237     Copyright   2009
   238   *}
   239   options [document = false]
   240   theories [quick_and_dirty] Nitpick_Examples
   241 
   242 session "HOL-Algebra" (main) in Algebra = HOL +
   243   description {*
   244     Author: Clemens Ballarin, started 24 September 1999
   245 
   246     The Isabelle Algebraic Library.
   247   *}
   248   options [document_graph]
   249   theories [document = false]
   250     (* Preliminaries from set and number theory *)
   251     "~~/src/HOL/Library/FuncSet"
   252     "~~/src/HOL/Old_Number_Theory/Primes"
   253     "~~/src/HOL/Library/Binomial"
   254     "~~/src/HOL/Library/Permutation"
   255   theories
   256     (*** New development, based on explicit structures ***)
   257     (* Groups *)
   258     FiniteProduct        (* Product operator for commutative groups *)
   259     Sylow                (* Sylow's theorem *)
   260     Bij                  (* Automorphism Groups *)
   261 
   262     (* Rings *)
   263     Divisibility         (* Rings *)
   264     IntRing              (* Ideals and residue classes *)
   265     UnivPoly             (* Polynomials *)
   266   theories [document = false]
   267     (*** Old development, based on axiomatic type classes ***)
   268     "abstract/Abstract"  (*The ring theory*)
   269     "poly/Polynomial"    (*The full theory*)
   270   files "document/root.bib" "document/root.tex"
   271 
   272 session "HOL-Auth" in Auth = HOL +
   273   description {*
   274     A new approach to verifying authentication protocols.
   275   *}
   276   options [document_graph]
   277   theories
   278     Auth_Shared
   279     Auth_Public
   280     "Smartcard/Auth_Smartcard"
   281     "Guard/Auth_Guard_Shared"
   282     "Guard/Auth_Guard_Public"
   283   files "document/root.tex"
   284 
   285 session "HOL-UNITY" in UNITY = "HOL-Auth" +
   286   description {*
   287     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   288     Copyright   1998  University of Cambridge
   289 
   290     Verifying security protocols using Chandy and Misra's UNITY formalism.
   291   *}
   292   options [document_graph]
   293   theories
   294     (*Basic meta-theory*)
   295     "UNITY_Main"
   296 
   297     (*Simple examples: no composition*)
   298     "Simple/Deadlock"
   299     "Simple/Common"
   300     "Simple/Network"
   301     "Simple/Token"
   302     "Simple/Channel"
   303     "Simple/Lift"
   304     "Simple/Mutex"
   305     "Simple/Reach"
   306     "Simple/Reachability"
   307 
   308     (*Verifying security protocols using UNITY*)
   309     "Simple/NSP_Bad"
   310 
   311     (*Example of composition*)
   312     "Comp/Handshake"
   313 
   314     (*Universal properties examples*)
   315     "Comp/Counter"
   316     "Comp/Counterc"
   317     "Comp/Priority"
   318 
   319     "Comp/TimerArray"
   320     "Comp/Progress"
   321 
   322     "Comp/Alloc"
   323     "Comp/AllocImpl"
   324     "Comp/Client"
   325 
   326     (*obsolete*)
   327     "ELT"
   328   files "document/root.tex"
   329 
   330 session "HOL-Unix" in Unix = HOL +
   331   options [print_mode = "no_brackets,no_type_brackets"]
   332   theories Unix
   333   files "document/root.bib" "document/root.tex"
   334 
   335 session "HOL-ZF" in ZF = HOL +
   336   theories MainZF Games
   337   files "document/root.tex"
   338 
   339 session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
   340   options [document_graph, print_mode = "iff,no_brackets"]
   341   theories [document = false]
   342     "~~/src/HOL/Library/Countable"
   343     "~~/src/HOL/Library/Monad_Syntax"
   344     "~~/src/HOL/Library/LaTeXsugar"
   345   theories Imperative_HOL_ex
   346   files "document/root.bib" "document/root.tex"
   347 
   348 session "HOL-Decision_Procs" in Decision_Procs = HOL +
   349   options [condition = ISABELLE_POLYML, document = false]
   350   theories Decision_Procs
   351 
   352 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
   353   options [document = false, proofs = 2, parallel_proofs = 0]
   354   theories Hilbert_Classical
   355 
   356 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
   357   description {*
   358     Examples for program extraction in Higher-Order Logic.
   359   *}
   360   options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0]
   361   theories [document = false]
   362     "~~/src/HOL/Library/Code_Target_Numeral"
   363     "~~/src/HOL/Library/Monad_Syntax"
   364     "~~/src/HOL/Number_Theory/Primes"
   365     "~~/src/HOL/Number_Theory/UniqueFactorization"
   366     "~~/src/HOL/Library/State_Monad"
   367   theories
   368     Greatest_Common_Divisor
   369     Warshall
   370     Higman_Extraction
   371     Pigeonhole
   372     Euclid
   373   files "document/root.bib" "document/root.tex"
   374 
   375 session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +
   376   description {*
   377     Lambda Calculus in de Bruijn's Notation.
   378 
   379     This session defines lambda-calculus terms with de Bruijn indixes and
   380     proves confluence of beta, eta and beta+eta.
   381 
   382     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
   383     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
   384   *}
   385   options [document_graph, print_mode = "no_brackets", proofs = 2, parallel_proofs = 0]
   386   theories [document = false]
   387     "~~/src/HOL/Library/Code_Target_Int"
   388   theories
   389     Eta
   390     StrongNorm
   391     Standardization
   392     WeakNorm
   393   files "document/root.bib" "document/root.tex"
   394 
   395 session "HOL-Prolog" in Prolog = HOL +
   396   description {*
   397     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
   398 
   399     A bare-bones implementation of Lambda-Prolog.
   400 
   401     This is a simple exploratory implementation of Lambda-Prolog in HOL,
   402     including some minimal examples (in Test.thy) and a more typical example of
   403     a little functional language and its type system.
   404   *}
   405   options [document = false]
   406   theories Test Type
   407 
   408 session "HOL-MicroJava" in MicroJava = HOL +
   409   description {*
   410     Formalization of a fragment of Java, together with a corresponding virtual
   411     machine and a specification of its bytecode verifier and a lightweight
   412     bytecode verifier, including proofs of type-safety.
   413   *}
   414   options [document_graph]
   415   theories [document = false] "~~/src/HOL/Library/While_Combinator"
   416   theories MicroJava
   417   files
   418     "document/introduction.tex"
   419     "document/root.bib"
   420     "document/root.tex"
   421 
   422 session "HOL-MicroJava-skip_proofs" in MicroJava = HOL +
   423   options [condition = ISABELLE_FULL_TEST, document = false, skip_proofs, quick_and_dirty]
   424   theories MicroJava
   425 
   426 session "HOL-NanoJava" in NanoJava = HOL +
   427   description {*
   428     Hoare Logic for a tiny fragment of Java.
   429   *}
   430   options [document_graph]
   431   theories Example
   432   files "document/root.bib" "document/root.tex"
   433 
   434 session "HOL-Bali" in Bali = HOL +
   435   options [document_graph]
   436   theories
   437     AxExample
   438     AxSound
   439     AxCompl
   440     Trans
   441   files "document/root.tex"
   442 
   443 session "HOL-IOA" in IOA = HOL +
   444   description {*
   445     Author:     Tobias Nipkow and Konrad Slind and Olaf Müller
   446     Copyright   1994--1996  TU Muenchen
   447 
   448     The meta theory of I/O-Automata in HOL. This formalization has been
   449     significantly changed and extended, see HOLCF/IOA. There are also the
   450     proofs of two communication protocols which formerly have been here.
   451 
   452     @inproceedings{Nipkow-Slind-IOA,
   453     author={Tobias Nipkow and Konrad Slind},
   454     title={{I/O} Automata in {Isabelle/HOL}},
   455     booktitle={Proc.\ TYPES Workshop 1994},
   456     publisher=Springer,
   457     series=LNCS,
   458     note={To appear}}
   459     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
   460 
   461     and
   462 
   463     @inproceedings{Mueller-Nipkow,
   464     author={Olaf M\"uller and Tobias Nipkow},
   465     title={Combining Model Checking and Deduction for {I/O}-Automata},
   466     booktitle={Proc.\ TACAS Workshop},
   467     organization={Aarhus University, BRICS report},
   468     year=1995}
   469     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
   470   *}
   471   options [document = false]
   472   theories Solve
   473 
   474 session "HOL-Lattice" in Lattice = HOL +
   475   description {*
   476     Author:     Markus Wenzel, TU Muenchen
   477 
   478     Basic theory of lattices and orders.
   479   *}
   480   theories CompleteLattice
   481   files "document/root.tex"
   482 
   483 session "HOL-ex" in ex = HOL +
   484   description {*
   485     Miscellaneous examples for Higher-Order Logic.
   486   *}
   487   options [timeout = 3600, condition = ISABELLE_POLYML]
   488   theories [document = false]
   489     "~~/src/HOL/Library/State_Monad"
   490     Code_Binary_Nat_examples
   491     "~~/src/HOL/Library/FuncSet"
   492     Eval_Examples
   493     Normalization_by_Evaluation
   494     Hebrew
   495     Chinese
   496     Serbian
   497     "~~/src/HOL/Library/FinFun_Syntax"
   498     "~~/src/HOL/Library/Refute"
   499   theories
   500     Iff_Oracle
   501     Coercion_Examples
   502     Numeral_Representation
   503     Higher_Order_Logic
   504     Abstract_NAT
   505     Guess
   506     Binary
   507     Fundefs
   508     Induction_Schema
   509     LocaleTest2
   510     Records
   511     While_Combinator_Example
   512     MonoidGroup
   513     BinEx
   514     Hex_Bin_Examples
   515     Antiquote
   516     Multiquote
   517     PER
   518     NatSum
   519     ThreeDivides
   520     Intuitionistic
   521     CTL
   522     Arith_Examples
   523     BT
   524     Tree23
   525     MergeSort
   526     Lagrange
   527     Groebner_Examples
   528     MT
   529     Unification
   530     Primrec
   531     Tarski
   532     Classical
   533     Set_Theory
   534     Meson_Test
   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   theories SVC_Oracle
   560   theories [condition = SVC_HOME]
   561     svc_test
   562   theories [condition = ZCHAFF_HOME]
   563     (*requires zChaff (or some other reasonably fast SAT solver)*)
   564     Sudoku
   565 (* FIXME
   566 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
   567 (*global side-effects ahead!*)
   568 try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)
   569 *)
   570   files "document/root.bib" "document/root.tex"
   571 
   572 session "HOL-Isar_Examples" in Isar_Examples = HOL +
   573   description {*
   574     Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
   575   *}
   576   theories [document = false]
   577     "~~/src/HOL/Library/Lattice_Syntax"
   578     "../Number_Theory/Primes"
   579   theories
   580     Basic_Logic
   581     Cantor
   582     Drinker
   583     Expr_Compiler
   584     Fibonacci
   585     Group
   586     Group_Context
   587     Group_Notepad
   588     Hoare_Ex
   589     Knaster_Tarski
   590     Mutilated_Checkerboard
   591     Nested_Datatype
   592     Peirce
   593     Puzzle
   594     Summation
   595   files
   596     "document/root.bib"
   597     "document/root.tex"
   598     "document/style.tex"
   599 
   600 session "HOL-SET_Protocol" in SET_Protocol = HOL +
   601   description {*
   602     Verification of the SET Protocol.
   603   *}
   604   options [document_graph]
   605   theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
   606   theories SET_Protocol
   607   files "document/root.tex"
   608 
   609 session "HOL-Matrix_LP" in Matrix_LP = HOL +
   610   description {*
   611     Two-dimensional matrices and linear programming.
   612   *}
   613   options [document_graph]
   614   theories Cplex
   615   files "document/root.tex"
   616 
   617 session "HOL-TLA" in TLA = HOL +
   618   description {*
   619     Lamport's Temporal Logic of Actions.
   620   *}
   621   options [document = false]
   622   theories TLA
   623 
   624 session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
   625   options [document = false]
   626   theories Inc
   627 
   628 session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
   629   options [document = false]
   630   theories DBuffer
   631 
   632 session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
   633   options [document = false]
   634   theories MemoryImplementation
   635 
   636 session "HOL-TPTP" in TPTP = HOL +
   637   description {*
   638     Author:     Jasmin Blanchette, TU Muenchen
   639     Author:     Nik Sultana, University of Cambridge
   640     Copyright   2011
   641 
   642     TPTP-related extensions.
   643   *}
   644   options [document = false]
   645   theories
   646     ATP_Theory_Export
   647     MaSh_Eval
   648     MaSh_Export
   649     TPTP_Interpret
   650     THF_Arith
   651   theories [proofs = 0]  (* FIXME !? *)
   652     ATP_Problem_Import
   653 
   654 session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +
   655   options [document_graph]
   656   theories
   657     Multivariate_Analysis
   658     Determinants
   659   files
   660     "document/root.tex"
   661 
   662 session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
   663   options [document_graph]
   664   theories [document = false]
   665     "~~/src/HOL/Library/Countable"
   666     "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
   667     "~~/src/HOL/Library/Permutation"
   668   theories
   669     Probability
   670     "ex/Dining_Cryptographers"
   671     "ex/Koepf_Duermuth_Countermeasure"
   672   files "document/root.tex"
   673 
   674 session "HOL-Nominal" (main) in Nominal = HOL +
   675   options [document = false]
   676   theories Nominal
   677 
   678 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
   679   options [timeout = 3600, condition = ISABELLE_POLYML, document = false]
   680   theories Nominal_Examples
   681   theories [quick_and_dirty] VC_Condition
   682 
   683 session "HOL-Cardinals-Base" in Cardinals = HOL +
   684   description {*
   685     Ordinals and Cardinals, Base Theories.
   686   *}
   687   options [document = false]
   688   theories Cardinal_Arithmetic
   689 
   690 session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" +
   691   description {*
   692     Ordinals and Cardinals, Full Theories.
   693   *}
   694   options [document = false]
   695   theories Cardinals
   696   files
   697     "document/intro.tex"
   698     "document/root.tex"
   699     "document/root.bib"
   700 
   701 session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-Base" +
   702   description {*
   703     Bounded Natural Functors for Datatypes.
   704   *}
   705   options [document = false]
   706   theories BNF_LFP
   707 
   708 session "HOL-BNF" in BNF = "HOL-Cardinals" +
   709   description {*
   710     Bounded Natural Functors for (Co)datatypes.
   711   *}
   712   options [document = false]
   713   theories BNF
   714 
   715 session "HOL-BNF-Examples" in "BNF/Examples" = "HOL-BNF" +
   716   description {*
   717     Examples for Bounded Natural Functors.
   718   *}
   719   options [document = false]
   720   theories
   721     Lambda_Term
   722     Process
   723     TreeFsetI
   724     "Derivation_Trees/Gram_Lang"
   725     "Derivation_Trees/Parallel"
   726     Koenig
   727   theories [condition = ISABELLE_FULL_TEST]
   728     Misc_Codata
   729     Misc_Data
   730 
   731 session "HOL-Word" (main) in Word = HOL +
   732   options [document_graph]
   733   theories Word
   734   files "document/root.bib" "document/root.tex"
   735 
   736 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   737   options [document = false]
   738   theories WordExamples
   739 
   740 session "HOL-Statespace" in Statespace = HOL +
   741   theories StateSpaceEx
   742   files "document/root.tex"
   743 
   744 session "HOL-NSA" in NSA = HOL +
   745   description {*
   746     Nonstandard analysis.
   747   *}
   748   options [document_graph]
   749   theories Hypercomplex
   750   files "document/root.tex"
   751 
   752 session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
   753   options [document = false]
   754   theories NSPrimes
   755 
   756 session "HOL-Mirabelle" in Mirabelle = HOL +
   757   options [document = false]
   758   theories Mirabelle_Test
   759 
   760 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   761   options [document = false, timeout = 60]
   762   theories Ex
   763 
   764 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
   765   options [document = false, quick_and_dirty]
   766   theories
   767     SMT_Examples
   768     SMT_Word_Examples
   769   theories [condition = ISABELLE_FULL_TEST]
   770     SMT_Tests
   771   files
   772     "SMT_Examples.certs"
   773     "SMT_Word_Examples.certs"
   774 
   775 session "HOL-Boogie" in "Boogie" = "HOL-Word" +
   776   options [document = false]
   777   theories Boogie
   778 
   779 session "HOL-Boogie-Examples" in "Boogie/Examples" = "HOL-Boogie" +
   780   options [document = false]
   781   theories
   782     Boogie_Max_Stepwise
   783     Boogie_Max
   784     Boogie_Dijkstra
   785     VCC_Max
   786   files
   787     "Boogie_Dijkstra.b2i"
   788     "Boogie_Dijkstra.certs"
   789     "Boogie_Max.b2i"
   790     "Boogie_Max.certs"
   791     "VCC_Max.b2i"
   792     "VCC_Max.certs"
   793 
   794 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   795   options [document = false]
   796   theories SPARK
   797 
   798 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   799   options [document = false]
   800   theories
   801     "Gcd/Greatest_Common_Divisor"
   802 
   803     "Liseq/Longest_Increasing_Subsequence"
   804 
   805     "RIPEMD-160/F"
   806     "RIPEMD-160/Hash"
   807     "RIPEMD-160/K_L"
   808     "RIPEMD-160/K_R"
   809     "RIPEMD-160/R_L"
   810     "RIPEMD-160/Round"
   811     "RIPEMD-160/R_R"
   812     "RIPEMD-160/S_L"
   813     "RIPEMD-160/S_R"
   814 
   815     "Sqrt/Sqrt"
   816   files
   817     "Gcd/greatest_common_divisor/g_c_d.fdl"
   818     "Gcd/greatest_common_divisor/g_c_d.rls"
   819     "Gcd/greatest_common_divisor/g_c_d.siv"
   820     "Liseq/liseq/liseq_length.fdl"
   821     "Liseq/liseq/liseq_length.rls"
   822     "Liseq/liseq/liseq_length.siv"
   823     "RIPEMD-160/rmd/f.fdl"
   824     "RIPEMD-160/rmd/f.rls"
   825     "RIPEMD-160/rmd/f.siv"
   826     "RIPEMD-160/rmd/hash.fdl"
   827     "RIPEMD-160/rmd/hash.rls"
   828     "RIPEMD-160/rmd/hash.siv"
   829     "RIPEMD-160/rmd/k_l.fdl"
   830     "RIPEMD-160/rmd/k_l.rls"
   831     "RIPEMD-160/rmd/k_l.siv"
   832     "RIPEMD-160/rmd/k_r.fdl"
   833     "RIPEMD-160/rmd/k_r.rls"
   834     "RIPEMD-160/rmd/k_r.siv"
   835     "RIPEMD-160/rmd/r_l.fdl"
   836     "RIPEMD-160/rmd/r_l.rls"
   837     "RIPEMD-160/rmd/r_l.siv"
   838     "RIPEMD-160/rmd/round.fdl"
   839     "RIPEMD-160/rmd/round.rls"
   840     "RIPEMD-160/rmd/round.siv"
   841     "RIPEMD-160/rmd/r_r.fdl"
   842     "RIPEMD-160/rmd/r_r.rls"
   843     "RIPEMD-160/rmd/r_r.siv"
   844     "RIPEMD-160/rmd/s_l.fdl"
   845     "RIPEMD-160/rmd/s_l.rls"
   846     "RIPEMD-160/rmd/s_l.siv"
   847     "RIPEMD-160/rmd/s_r.fdl"
   848     "RIPEMD-160/rmd/s_r.rls"
   849     "RIPEMD-160/rmd/s_r.siv"
   850 
   851 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   852   options [show_question_marks = false]
   853   theories
   854     Example_Verification
   855     VC_Principles
   856     Reference
   857     Complex_Types
   858   files
   859     "complex_types_app/initialize.fdl"
   860     "complex_types_app/initialize.rls"
   861     "complex_types_app/initialize.siv"
   862     "document/complex_types.ads"
   863     "document/complex_types_app.adb"
   864     "document/complex_types_app.ads"
   865     "document/Gcd.adb"
   866     "document/Gcd.ads"
   867     "document/intro.tex"
   868     "document/loop_invariant.adb"
   869     "document/loop_invariant.ads"
   870     "document/root.bib"
   871     "document/root.tex"
   872     "document/Simple_Gcd.adb"
   873     "document/Simple_Gcd.ads"
   874     "loop_invariant/proc1.fdl"
   875     "loop_invariant/proc1.rls"
   876     "loop_invariant/proc1.siv"
   877     "loop_invariant/proc2.fdl"
   878     "loop_invariant/proc2.rls"
   879     "loop_invariant/proc2.siv"
   880     "simple_greatest_common_divisor/g_c_d.fdl"
   881     "simple_greatest_common_divisor/g_c_d.rls"
   882     "simple_greatest_common_divisor/g_c_d.siv"
   883 
   884 session "HOL-Mutabelle" in Mutabelle = HOL +
   885   options [document = false]
   886   theories MutabelleExtra
   887 
   888 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
   889   options [document = false]
   890   theories
   891     Quickcheck_Examples
   892   (* FIXME
   893     Quickcheck_Lattice_Examples
   894     Completeness
   895     Quickcheck_Interfaces
   896     Hotel_Example *)
   897   theories [condition = ISABELLE_GHC]
   898     Quickcheck_Narrowing_Examples
   899 
   900 session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
   901   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
   902     Find_Unused_Assms_Examples
   903     Needham_Schroeder_No_Attacker_Example
   904     Needham_Schroeder_Guided_Attacker_Example
   905     Needham_Schroeder_Unguided_Attacker_Example
   906 
   907 session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
   908   description {*
   909     Author:     Cezary Kaliszyk and Christian Urban
   910   *}
   911   options [document = false]
   912   theories
   913     DList
   914     FSet
   915     Quotient_Int
   916     Quotient_Message
   917     Lift_FSet
   918     Lift_Set
   919     Lift_Fun
   920     Quotient_Rat
   921     Lift_DList
   922 
   923 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   924   options [document = false]
   925   theories
   926     Examples
   927     Predicate_Compile_Tests
   928     (* FIXME
   929     Predicate_Compile_Quickcheck_Examples  -- should be added again soon (since 21-Oct-2010) *)
   930     Specialisation_Examples
   931     (* FIXME since 21-Jul-2011
   932     Hotel_Example_Small_Generator
   933     IMP_1
   934     IMP_2
   935     IMP_3
   936     IMP_4 *)
   937   theories [condition = "ISABELLE_SWIPL"]  (* FIXME: *or* ISABELLE_YAP (??) *)
   938     Code_Prolog_Examples
   939     Context_Free_Grammar_Example
   940     Hotel_Example_Prolog
   941     Lambda_Example
   942     List_Examples
   943   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]  (* FIXME: *or* ISABELLE_YAP (??) *)
   944     Reg_Exp_Example
   945 
   946 session HOLCF (main) in HOLCF = HOL +
   947   description {*
   948     Author:     Franz Regensburger
   949     Author:     Brian Huffman
   950 
   951     HOLCF -- a semantic extension of HOL by the LCF logic.
   952   *}
   953   options [document_graph]
   954   theories [document = false]
   955     "~~/src/HOL/Library/Nat_Bijection"
   956     "~~/src/HOL/Library/Countable"
   957   theories
   958     Plain_HOLCF
   959     Fixrec
   960     HOLCF
   961   files "document/root.tex"
   962 
   963 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   964   theories
   965     Domain_ex
   966     Fixrec_ex
   967     New_Domain
   968   files "document/root.tex"
   969 
   970 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   971   options [document = false]
   972   theories HOLCF_Library
   973 
   974 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   975   description {*
   976     IMP -- A WHILE-language and its Semantics.
   977 
   978     This is the HOLCF-based denotational semantics of a simple WHILE-language.
   979   *}
   980   options [document = false]
   981   theories HoareEx
   982   files "document/root.tex"
   983 
   984 session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
   985   description {*
   986     Miscellaneous examples for HOLCF.
   987   *}
   988   options [document = false]
   989   theories
   990     Dnat
   991     Dagstuhl
   992     Focus_ex
   993     Fix2
   994     Hoare
   995     Concurrency_Monad
   996     Loop
   997     Powerdomain_ex
   998     Domain_Proofs
   999     Letrec
  1000     Pattern_Match
  1001 
  1002 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
  1003   description {*
  1004     FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
  1005 
  1006     For introductions to FOCUS, see
  1007 
  1008     "The Design of Distributed Systems - An Introduction to FOCUS"
  1009     http://www4.in.tum.de/publ/html.php?e=2
  1010 
  1011     "Specification and Refinement of a Buffer of Length One"
  1012     http://www4.in.tum.de/publ/html.php?e=15
  1013 
  1014     "Specification and Development of Interactive Systems: Focus on Streams,
  1015     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
  1016   *}
  1017   options [document = false]
  1018   theories
  1019     Fstreams
  1020     FOCUS
  1021     Buffer_adm
  1022 
  1023 session IOA in "HOLCF/IOA" = HOLCF +
  1024   description {*
  1025     Author:     Olaf Mueller
  1026     Copyright   1997 TU München
  1027 
  1028     A formalization of I/O automata in HOLCF.
  1029 
  1030     The distribution contains simulation relations, temporal logic, and an
  1031     abstraction theory. Everything is based upon a domain-theoretic model of
  1032     finite and infinite sequences.
  1033   *}
  1034   options [document = false]
  1035   theories "meta_theory/Abstraction"
  1036 
  1037 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  1038   description {*
  1039     Author:     Olaf Mueller
  1040 
  1041     The Alternating Bit Protocol performed in I/O-Automata.
  1042   *}
  1043   options [document = false]
  1044   theories Correctness
  1045 
  1046 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
  1047   description {*
  1048     Author:     Tobias Nipkow & Konrad Slind
  1049 
  1050     A network transmission protocol, performed in the
  1051     I/O automata formalization by Olaf Mueller.
  1052   *}
  1053   options [document = false]
  1054   theories Correctness
  1055 
  1056 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
  1057   description {*
  1058     Author:     Olaf Mueller
  1059 
  1060     Memory storage case study.
  1061   *}
  1062   options [document = false]
  1063   theories Correctness
  1064 
  1065 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
  1066   description {*
  1067     Author:     Olaf Mueller
  1068   *}
  1069   options [document = false]
  1070   theories
  1071     TrivEx
  1072     TrivEx2
  1073 
  1074 session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
  1075   description {*
  1076     Some rather large datatype examples (from John Harrison).
  1077   *}
  1078   options [document = false]
  1079   theories [condition = ISABELLE_FULL_TEST, timing]
  1080     Brackin
  1081     Instructions
  1082     SML
  1083     Verilog
  1084 
  1085 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
  1086   description {*
  1087     Some benchmark on large record.
  1088   *}
  1089   options [document = false]
  1090   theories [condition = ISABELLE_FULL_TEST, timing]
  1091     Record_Benchmark
  1092