src/HOL/ROOT
author wenzelm
Wed Mar 27 16:38:25 2013 +0100 (2013-03-27)
changeset 51553 63327f679cff
parent 51544 8c58fbbc1d5a
child 51558 91f8bed6d0a4
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
     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
   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, 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, 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, parallel_proofs = 0]
   390   theories [document = false]
   391     "~~/src/HOL/Library/Code_Target_Int"
   392   theories
   393     Eta
   394     StrongNorm
   395     Standardization
   396     WeakNorm
   397   files "document/root.bib" "document/root.tex"
   398 
   399 session "HOL-Prolog" in Prolog = HOL +
   400   description {*
   401     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
   402 
   403     A bare-bones implementation of Lambda-Prolog.
   404 
   405     This is a simple exploratory implementation of Lambda-Prolog in HOL,
   406     including some minimal examples (in Test.thy) and a more typical example of
   407     a little functional language and its type system.
   408   *}
   409   options [document = false]
   410   theories Test Type
   411 
   412 session "HOL-MicroJava" in MicroJava = HOL +
   413   description {*
   414     Formalization of a fragment of Java, together with a corresponding virtual
   415     machine and a specification of its bytecode verifier and a lightweight
   416     bytecode verifier, including proofs of type-safety.
   417   *}
   418   options [document_graph]
   419   theories [document = false] "~~/src/HOL/Library/While_Combinator"
   420   theories MicroJava
   421   files
   422     "document/introduction.tex"
   423     "document/root.bib"
   424     "document/root.tex"
   425 
   426 session "HOL-MicroJava-skip_proofs" in MicroJava = HOL +
   427   options [condition = ISABELLE_FULL_TEST, document = false, skip_proofs]
   428   theories MicroJava
   429 
   430 session "HOL-NanoJava" in NanoJava = HOL +
   431   description {*
   432     Hoare Logic for a tiny fragment of Java.
   433   *}
   434   options [document_graph]
   435   theories Example
   436   files "document/root.bib" "document/root.tex"
   437 
   438 session "HOL-Bali" in Bali = HOL +
   439   options [document_graph]
   440   theories
   441     AxExample
   442     AxSound
   443     AxCompl
   444     Trans
   445   files "document/root.tex"
   446 
   447 session "HOL-IOA" in IOA = HOL +
   448   description {*
   449     Author:     Tobias Nipkow and Konrad Slind and Olaf Müller
   450     Copyright   1994--1996  TU Muenchen
   451 
   452     The meta theory of I/O-Automata in HOL. This formalization has been
   453     significantly changed and extended, see HOLCF/IOA. There are also the
   454     proofs of two communication protocols which formerly have been here.
   455 
   456     @inproceedings{Nipkow-Slind-IOA,
   457     author={Tobias Nipkow and Konrad Slind},
   458     title={{I/O} Automata in {Isabelle/HOL}},
   459     booktitle={Proc.\ TYPES Workshop 1994},
   460     publisher=Springer,
   461     series=LNCS,
   462     note={To appear}}
   463     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
   464 
   465     and
   466 
   467     @inproceedings{Mueller-Nipkow,
   468     author={Olaf M\"uller and Tobias Nipkow},
   469     title={Combining Model Checking and Deduction for {I/O}-Automata},
   470     booktitle={Proc.\ TACAS Workshop},
   471     organization={Aarhus University, BRICS report},
   472     year=1995}
   473     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
   474   *}
   475   options [document = false]
   476   theories Solve
   477 
   478 session "HOL-Lattice" in Lattice = HOL +
   479   description {*
   480     Author:     Markus Wenzel, TU Muenchen
   481 
   482     Basic theory of lattices and orders.
   483   *}
   484   theories CompleteLattice
   485   files "document/root.tex"
   486 
   487 session "HOL-ex" in ex = HOL +
   488   description {*
   489     Miscellaneous examples for Higher-Order Logic.
   490   *}
   491   options [timeout = 3600, condition = ISABELLE_POLYML]
   492   theories [document = false]
   493     "~~/src/HOL/Library/State_Monad"
   494     Code_Binary_Nat_examples
   495     "~~/src/HOL/Library/FuncSet"
   496     Eval_Examples
   497     Normalization_by_Evaluation
   498     Hebrew
   499     Chinese
   500     Serbian
   501     "~~/src/HOL/Library/FinFun_Syntax"
   502     "~~/src/HOL/Library/Refute"
   503   theories
   504     Iff_Oracle
   505     Coercion_Examples
   506     Numeral_Representation
   507     Higher_Order_Logic
   508     Abstract_NAT
   509     Guess
   510     Binary
   511     Fundefs
   512     Induction_Schema
   513     LocaleTest2
   514     Records
   515     While_Combinator_Example
   516     MonoidGroup
   517     BinEx
   518     Hex_Bin_Examples
   519     Antiquote
   520     Multiquote
   521     PER
   522     NatSum
   523     ThreeDivides
   524     Intuitionistic
   525     CTL
   526     Arith_Examples
   527     BT
   528     Tree23
   529     MergeSort
   530     Lagrange
   531     Groebner_Examples
   532     MT
   533     Unification
   534     Primrec
   535     Tarski
   536     Classical
   537     Set_Theory
   538     Meson_Test
   539     Termination
   540     Coherent
   541     PresburgerEx
   542     Reflection_Examples
   543     Sqrt
   544     Sqrt_Script
   545     Transfer_Ex
   546     Transfer_Int_Nat
   547     HarmonicSeries
   548     Refute_Examples
   549     Execute_Choice
   550     Summation
   551     Gauge_Integration
   552     Dedekind_Real
   553     Quicksort
   554     Birthday_Paradox
   555     List_to_Set_Comprehension_Examples
   556     Seq
   557     Simproc_Tests
   558     Executable_Relation
   559     FinFunPred
   560     Set_Comprehension_Pointfree_Tests
   561     Parallel_Example
   562     IArray_Examples
   563   theories SVC_Oracle
   564   theories [condition = SVC_HOME]
   565     svc_test
   566   theories [condition = ZCHAFF_HOME]
   567     (*requires zChaff (or some other reasonably fast SAT solver)*)
   568     Sudoku
   569 (* FIXME
   570 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
   571 (*global side-effects ahead!*)
   572 try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)
   573 *)
   574   files "document/root.bib" "document/root.tex"
   575 
   576 session "HOL-Isar_Examples" in Isar_Examples = HOL +
   577   description {*
   578     Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
   579   *}
   580   theories [document = false]
   581     "~~/src/HOL/Library/Lattice_Syntax"
   582     "../Number_Theory/Primes"
   583   theories
   584     Basic_Logic
   585     Cantor
   586     Drinker
   587     Expr_Compiler
   588     Fibonacci
   589     Group
   590     Group_Context
   591     Group_Notepad
   592     Hoare_Ex
   593     Knaster_Tarski
   594     Mutilated_Checkerboard
   595     Nested_Datatype
   596     Peirce
   597     Puzzle
   598     Summation
   599   files
   600     "document/root.bib"
   601     "document/root.tex"
   602     "document/style.tex"
   603 
   604 session "HOL-SET_Protocol" in SET_Protocol = HOL +
   605   description {*
   606     Verification of the SET Protocol.
   607   *}
   608   options [document_graph]
   609   theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
   610   theories SET_Protocol
   611   files "document/root.tex"
   612 
   613 session "HOL-Matrix_LP" in Matrix_LP = HOL +
   614   description {*
   615     Two-dimensional matrices and linear programming.
   616   *}
   617   options [document_graph]
   618   theories Cplex
   619   files "document/root.tex"
   620 
   621 session "HOL-TLA" in TLA = HOL +
   622   description {*
   623     Lamport's Temporal Logic of Actions.
   624   *}
   625   options [document = false]
   626   theories TLA
   627 
   628 session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
   629   options [document = false]
   630   theories Inc
   631 
   632 session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
   633   options [document = false]
   634   theories DBuffer
   635 
   636 session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
   637   options [document = false]
   638   theories MemoryImplementation
   639 
   640 session "HOL-TPTP" in TPTP = HOL +
   641   description {*
   642     Author:     Jasmin Blanchette, TU Muenchen
   643     Author:     Nik Sultana, University of Cambridge
   644     Copyright   2011
   645 
   646     TPTP-related extensions.
   647   *}
   648   options [document = false]
   649   theories
   650     ATP_Theory_Export
   651     MaSh_Eval
   652     MaSh_Export
   653     TPTP_Interpret
   654     THF_Arith
   655   theories [proofs = 0]  (* FIXME !? *)
   656     ATP_Problem_Import
   657 
   658 session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +
   659   options [document_graph]
   660   theories
   661     Multivariate_Analysis
   662     Determinants
   663   files
   664     "document/root.tex"
   665 
   666 session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
   667   options [document_graph]
   668   theories [document = false]
   669     "~~/src/HOL/Library/Countable"
   670     "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
   671     "~~/src/HOL/Library/Permutation"
   672   theories
   673     Probability
   674     "ex/Dining_Cryptographers"
   675     "ex/Koepf_Duermuth_Countermeasure"
   676   files "document/root.tex"
   677 
   678 session "HOL-Nominal" (main) in Nominal = HOL +
   679   options [document = false]
   680   theories Nominal
   681 
   682 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
   683   options [timeout = 3600, condition = ISABELLE_POLYML, document = false]
   684   theories Nominal_Examples
   685   theories [quick_and_dirty] VC_Condition
   686 
   687 session "HOL-Cardinals-Base" in Cardinals = HOL +
   688   description {*
   689     Ordinals and Cardinals, Base Theories.
   690   *}
   691   options [document = false]
   692   theories Cardinal_Arithmetic
   693 
   694 session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" +
   695   description {*
   696     Ordinals and Cardinals, Full Theories.
   697   *}
   698   options [document = false]
   699   theories Cardinals
   700   files
   701     "document/intro.tex"
   702     "document/root.tex"
   703     "document/root.bib"
   704 
   705 session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-Base" +
   706   description {*
   707     Bounded Natural Functors for Datatypes.
   708   *}
   709   options [document = false]
   710   theories BNF_LFP
   711 
   712 session "HOL-BNF" in BNF = "HOL-Cardinals" +
   713   description {*
   714     Bounded Natural Functors for (Co)datatypes.
   715   *}
   716   options [document = false]
   717   theories BNF
   718 
   719 session "HOL-BNF-Examples" in "BNF/Examples" = "HOL-BNF" +
   720   description {*
   721     Examples for Bounded Natural Functors.
   722   *}
   723   options [document = false]
   724   theories
   725     Lambda_Term
   726     Process
   727     TreeFsetI
   728     "Derivation_Trees/Gram_Lang"
   729     "Derivation_Trees/Parallel"
   730     Koenig
   731   theories [condition = ISABELLE_FULL_TEST]
   732     Misc_Codata
   733     Misc_Data
   734 
   735 session "HOL-Word" (main) in Word = HOL +
   736   options [document_graph]
   737   theories Word
   738   files "document/root.bib" "document/root.tex"
   739 
   740 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   741   options [document = false]
   742   theories WordExamples
   743 
   744 session "HOL-Statespace" in Statespace = HOL +
   745   theories StateSpaceEx
   746   files "document/root.tex"
   747 
   748 session "HOL-NSA" in NSA = HOL +
   749   description {*
   750     Nonstandard analysis.
   751   *}
   752   options [document_graph]
   753   theories Hypercomplex
   754   files "document/root.tex"
   755 
   756 session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
   757   options [document = false]
   758   theories NSPrimes
   759 
   760 session "HOL-Mirabelle" in Mirabelle = HOL +
   761   options [document = false]
   762   theories Mirabelle_Test
   763 
   764 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   765   options [document = false, timeout = 60]
   766   theories Ex
   767 
   768 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
   769   options [document = false, quick_and_dirty]
   770   theories
   771     SMT_Examples
   772     SMT_Word_Examples
   773   theories [condition = ISABELLE_FULL_TEST]
   774     SMT_Tests
   775   files
   776     "SMT_Examples.certs"
   777     "SMT_Word_Examples.certs"
   778 
   779 session "HOL-Boogie" in "Boogie" = "HOL-Word" +
   780   options [document = false]
   781   theories Boogie
   782 
   783 session "HOL-Boogie-Examples" in "Boogie/Examples" = "HOL-Boogie" +
   784   options [document = false]
   785   theories
   786     Boogie_Max_Stepwise
   787     Boogie_Max
   788     Boogie_Dijkstra
   789     VCC_Max
   790   files
   791     "Boogie_Dijkstra.b2i"
   792     "Boogie_Dijkstra.certs"
   793     "Boogie_Max.b2i"
   794     "Boogie_Max.certs"
   795     "VCC_Max.b2i"
   796     "VCC_Max.certs"
   797 
   798 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   799   options [document = false]
   800   theories SPARK
   801 
   802 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   803   options [document = false]
   804   theories
   805     "Gcd/Greatest_Common_Divisor"
   806 
   807     "Liseq/Longest_Increasing_Subsequence"
   808 
   809     "RIPEMD-160/F"
   810     "RIPEMD-160/Hash"
   811     "RIPEMD-160/K_L"
   812     "RIPEMD-160/K_R"
   813     "RIPEMD-160/R_L"
   814     "RIPEMD-160/Round"
   815     "RIPEMD-160/R_R"
   816     "RIPEMD-160/S_L"
   817     "RIPEMD-160/S_R"
   818 
   819     "Sqrt/Sqrt"
   820   files
   821     "Gcd/greatest_common_divisor/g_c_d.fdl"
   822     "Gcd/greatest_common_divisor/g_c_d.rls"
   823     "Gcd/greatest_common_divisor/g_c_d.siv"
   824     "Liseq/liseq/liseq_length.fdl"
   825     "Liseq/liseq/liseq_length.rls"
   826     "Liseq/liseq/liseq_length.siv"
   827     "RIPEMD-160/rmd/f.fdl"
   828     "RIPEMD-160/rmd/f.rls"
   829     "RIPEMD-160/rmd/f.siv"
   830     "RIPEMD-160/rmd/hash.fdl"
   831     "RIPEMD-160/rmd/hash.rls"
   832     "RIPEMD-160/rmd/hash.siv"
   833     "RIPEMD-160/rmd/k_l.fdl"
   834     "RIPEMD-160/rmd/k_l.rls"
   835     "RIPEMD-160/rmd/k_l.siv"
   836     "RIPEMD-160/rmd/k_r.fdl"
   837     "RIPEMD-160/rmd/k_r.rls"
   838     "RIPEMD-160/rmd/k_r.siv"
   839     "RIPEMD-160/rmd/r_l.fdl"
   840     "RIPEMD-160/rmd/r_l.rls"
   841     "RIPEMD-160/rmd/r_l.siv"
   842     "RIPEMD-160/rmd/round.fdl"
   843     "RIPEMD-160/rmd/round.rls"
   844     "RIPEMD-160/rmd/round.siv"
   845     "RIPEMD-160/rmd/r_r.fdl"
   846     "RIPEMD-160/rmd/r_r.rls"
   847     "RIPEMD-160/rmd/r_r.siv"
   848     "RIPEMD-160/rmd/s_l.fdl"
   849     "RIPEMD-160/rmd/s_l.rls"
   850     "RIPEMD-160/rmd/s_l.siv"
   851     "RIPEMD-160/rmd/s_r.fdl"
   852     "RIPEMD-160/rmd/s_r.rls"
   853     "RIPEMD-160/rmd/s_r.siv"
   854 
   855 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   856   options [show_question_marks = false]
   857   theories
   858     Example_Verification
   859     VC_Principles
   860     Reference
   861     Complex_Types
   862   files
   863     "complex_types_app/initialize.fdl"
   864     "complex_types_app/initialize.rls"
   865     "complex_types_app/initialize.siv"
   866     "document/complex_types.ads"
   867     "document/complex_types_app.adb"
   868     "document/complex_types_app.ads"
   869     "document/Gcd.adb"
   870     "document/Gcd.ads"
   871     "document/intro.tex"
   872     "document/loop_invariant.adb"
   873     "document/loop_invariant.ads"
   874     "document/root.bib"
   875     "document/root.tex"
   876     "document/Simple_Gcd.adb"
   877     "document/Simple_Gcd.ads"
   878     "loop_invariant/proc1.fdl"
   879     "loop_invariant/proc1.rls"
   880     "loop_invariant/proc1.siv"
   881     "loop_invariant/proc2.fdl"
   882     "loop_invariant/proc2.rls"
   883     "loop_invariant/proc2.siv"
   884     "simple_greatest_common_divisor/g_c_d.fdl"
   885     "simple_greatest_common_divisor/g_c_d.rls"
   886     "simple_greatest_common_divisor/g_c_d.siv"
   887 
   888 session "HOL-Mutabelle" in Mutabelle = HOL +
   889   options [document = false]
   890   theories MutabelleExtra
   891 
   892 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
   893   options [document = false]
   894   theories
   895     Quickcheck_Examples
   896   (* FIXME
   897     Quickcheck_Lattice_Examples
   898     Completeness
   899     Quickcheck_Interfaces
   900     Hotel_Example *)
   901   theories [condition = ISABELLE_GHC]
   902     Quickcheck_Narrowing_Examples
   903 
   904 session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
   905   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
   906     Find_Unused_Assms_Examples
   907     Needham_Schroeder_No_Attacker_Example
   908     Needham_Schroeder_Guided_Attacker_Example
   909     Needham_Schroeder_Unguided_Attacker_Example
   910 
   911 session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
   912   description {*
   913     Author:     Cezary Kaliszyk and Christian Urban
   914   *}
   915   options [document = false]
   916   theories
   917     DList
   918     FSet
   919     Quotient_Int
   920     Quotient_Message
   921     Lift_FSet
   922     Lift_Set
   923     Lift_Fun
   924     Quotient_Rat
   925     Lift_DList
   926 
   927 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   928   options [document = false]
   929   theories
   930     Examples
   931     Predicate_Compile_Tests
   932     (* FIXME
   933     Predicate_Compile_Quickcheck_Examples  -- should be added again soon (since 21-Oct-2010) *)
   934     Specialisation_Examples
   935     (* FIXME since 21-Jul-2011
   936     Hotel_Example_Small_Generator
   937     IMP_1
   938     IMP_2
   939     IMP_3
   940     IMP_4 *)
   941   theories [condition = "ISABELLE_SWIPL"]  (* FIXME: *or* ISABELLE_YAP (??) *)
   942     Code_Prolog_Examples
   943     Context_Free_Grammar_Example
   944     Hotel_Example_Prolog
   945     Lambda_Example
   946     List_Examples
   947   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]  (* FIXME: *or* ISABELLE_YAP (??) *)
   948     Reg_Exp_Example
   949 
   950 session HOLCF (main) in HOLCF = HOL +
   951   description {*
   952     Author:     Franz Regensburger
   953     Author:     Brian Huffman
   954 
   955     HOLCF -- a semantic extension of HOL by the LCF logic.
   956   *}
   957   options [document_graph]
   958   theories [document = false]
   959     "~~/src/HOL/Library/Nat_Bijection"
   960     "~~/src/HOL/Library/Countable"
   961   theories
   962     Plain_HOLCF
   963     Fixrec
   964     HOLCF
   965   files "document/root.tex"
   966 
   967 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   968   theories
   969     Domain_ex
   970     Fixrec_ex
   971     New_Domain
   972   files "document/root.tex"
   973 
   974 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   975   options [document = false]
   976   theories HOLCF_Library
   977 
   978 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   979   description {*
   980     IMP -- A WHILE-language and its Semantics.
   981 
   982     This is the HOLCF-based denotational semantics of a simple WHILE-language.
   983   *}
   984   options [document = false]
   985   theories HoareEx
   986   files "document/root.tex"
   987 
   988 session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
   989   description {*
   990     Miscellaneous examples for HOLCF.
   991   *}
   992   options [document = false]
   993   theories
   994     Dnat
   995     Dagstuhl
   996     Focus_ex
   997     Fix2
   998     Hoare
   999     Concurrency_Monad
  1000     Loop
  1001     Powerdomain_ex
  1002     Domain_Proofs
  1003     Letrec
  1004     Pattern_Match
  1005 
  1006 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
  1007   description {*
  1008     FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
  1009 
  1010     For introductions to FOCUS, see
  1011 
  1012     "The Design of Distributed Systems - An Introduction to FOCUS"
  1013     http://www4.in.tum.de/publ/html.php?e=2
  1014 
  1015     "Specification and Refinement of a Buffer of Length One"
  1016     http://www4.in.tum.de/publ/html.php?e=15
  1017 
  1018     "Specification and Development of Interactive Systems: Focus on Streams,
  1019     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
  1020   *}
  1021   options [document = false]
  1022   theories
  1023     Fstreams
  1024     FOCUS
  1025     Buffer_adm
  1026 
  1027 session IOA in "HOLCF/IOA" = HOLCF +
  1028   description {*
  1029     Author:     Olaf Mueller
  1030     Copyright   1997 TU München
  1031 
  1032     A formalization of I/O automata in HOLCF.
  1033 
  1034     The distribution contains simulation relations, temporal logic, and an
  1035     abstraction theory. Everything is based upon a domain-theoretic model of
  1036     finite and infinite sequences.
  1037   *}
  1038   options [document = false]
  1039   theories "meta_theory/Abstraction"
  1040 
  1041 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  1042   description {*
  1043     Author:     Olaf Mueller
  1044 
  1045     The Alternating Bit Protocol performed in I/O-Automata.
  1046   *}
  1047   options [document = false]
  1048   theories Correctness
  1049 
  1050 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
  1051   description {*
  1052     Author:     Tobias Nipkow & Konrad Slind
  1053 
  1054     A network transmission protocol, performed in the
  1055     I/O automata formalization by Olaf Mueller.
  1056   *}
  1057   options [document = false]
  1058   theories Correctness
  1059 
  1060 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
  1061   description {*
  1062     Author:     Olaf Mueller
  1063 
  1064     Memory storage case study.
  1065   *}
  1066   options [document = false]
  1067   theories Correctness
  1068 
  1069 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
  1070   description {*
  1071     Author:     Olaf Mueller
  1072   *}
  1073   options [document = false]
  1074   theories
  1075     TrivEx
  1076     TrivEx2
  1077 
  1078 session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
  1079   description {*
  1080     Some rather large datatype examples (from John Harrison).
  1081   *}
  1082   options [document = false]
  1083   theories [condition = ISABELLE_FULL_TEST, timing]
  1084     Brackin
  1085     Instructions
  1086     SML
  1087     Verilog
  1088 
  1089 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
  1090   description {*
  1091     Some benchmark on large record.
  1092   *}
  1093   options [document = false]
  1094   theories [condition = ISABELLE_FULL_TEST, timing]
  1095     Record_Benchmark
  1096