src/HOL/ROOT
author ballarin
Mon Mar 25 20:00:27 2013 +0100 (2013-03-25)
changeset 51517 7957d26c3334
parent 51422 821a70e29e0b
child 51544 8c58fbbc1d5a
permissions -rw-r--r--
Discontinued theories src/HOL/Algebra/abstract and .../poly.
     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   options [condition = ISABELLE_POLYML, document = false]
   351   theories Decision_Procs
   352 
   353 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
   354   options [document = false, proofs = 2, parallel_proofs = 0]
   355   theories Hilbert_Classical
   356 
   357 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
   358   description {*
   359     Examples for program extraction in Higher-Order Logic.
   360   *}
   361   options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0]
   362   theories [document = false]
   363     "~~/src/HOL/Library/Code_Target_Numeral"
   364     "~~/src/HOL/Library/Monad_Syntax"
   365     "~~/src/HOL/Number_Theory/Primes"
   366     "~~/src/HOL/Number_Theory/UniqueFactorization"
   367     "~~/src/HOL/Library/State_Monad"
   368   theories
   369     Greatest_Common_Divisor
   370     Warshall
   371     Higman_Extraction
   372     Pigeonhole
   373     Euclid
   374   files "document/root.bib" "document/root.tex"
   375 
   376 session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +
   377   description {*
   378     Lambda Calculus in de Bruijn's Notation.
   379 
   380     This session defines lambda-calculus terms with de Bruijn indixes and
   381     proves confluence of beta, eta and beta+eta.
   382 
   383     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
   384     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
   385   *}
   386   options [document_graph, print_mode = "no_brackets", proofs = 2, parallel_proofs = 0]
   387   theories [document = false]
   388     "~~/src/HOL/Library/Code_Target_Int"
   389   theories
   390     Eta
   391     StrongNorm
   392     Standardization
   393     WeakNorm
   394   files "document/root.bib" "document/root.tex"
   395 
   396 session "HOL-Prolog" in Prolog = HOL +
   397   description {*
   398     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
   399 
   400     A bare-bones implementation of Lambda-Prolog.
   401 
   402     This is a simple exploratory implementation of Lambda-Prolog in HOL,
   403     including some minimal examples (in Test.thy) and a more typical example of
   404     a little functional language and its type system.
   405   *}
   406   options [document = false]
   407   theories Test Type
   408 
   409 session "HOL-MicroJava" in MicroJava = HOL +
   410   description {*
   411     Formalization of a fragment of Java, together with a corresponding virtual
   412     machine and a specification of its bytecode verifier and a lightweight
   413     bytecode verifier, including proofs of type-safety.
   414   *}
   415   options [document_graph]
   416   theories [document = false] "~~/src/HOL/Library/While_Combinator"
   417   theories MicroJava
   418   files
   419     "document/introduction.tex"
   420     "document/root.bib"
   421     "document/root.tex"
   422 
   423 session "HOL-MicroJava-skip_proofs" in MicroJava = HOL +
   424   options [condition = ISABELLE_FULL_TEST, document = false, skip_proofs, quick_and_dirty]
   425   theories MicroJava
   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     Meson_Test
   536     Termination
   537     Coherent
   538     PresburgerEx
   539     Reflection_Examples
   540     Sqrt
   541     Sqrt_Script
   542     Transfer_Ex
   543     Transfer_Int_Nat
   544     HarmonicSeries
   545     Refute_Examples
   546     Execute_Choice
   547     Summation
   548     Gauge_Integration
   549     Dedekind_Real
   550     Quicksort
   551     Birthday_Paradox
   552     List_to_Set_Comprehension_Examples
   553     Seq
   554     Simproc_Tests
   555     Executable_Relation
   556     FinFunPred
   557     Set_Comprehension_Pointfree_Tests
   558     Parallel_Example
   559     IArray_Examples
   560   theories SVC_Oracle
   561   theories [condition = SVC_HOME]
   562     svc_test
   563   theories [condition = ZCHAFF_HOME]
   564     (*requires zChaff (or some other reasonably fast SAT solver)*)
   565     Sudoku
   566 (* FIXME
   567 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
   568 (*global side-effects ahead!*)
   569 try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)
   570 *)
   571   files "document/root.bib" "document/root.tex"
   572 
   573 session "HOL-Isar_Examples" in Isar_Examples = HOL +
   574   description {*
   575     Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
   576   *}
   577   theories [document = false]
   578     "~~/src/HOL/Library/Lattice_Syntax"
   579     "../Number_Theory/Primes"
   580   theories
   581     Basic_Logic
   582     Cantor
   583     Drinker
   584     Expr_Compiler
   585     Fibonacci
   586     Group
   587     Group_Context
   588     Group_Notepad
   589     Hoare_Ex
   590     Knaster_Tarski
   591     Mutilated_Checkerboard
   592     Nested_Datatype
   593     Peirce
   594     Puzzle
   595     Summation
   596   files
   597     "document/root.bib"
   598     "document/root.tex"
   599     "document/style.tex"
   600 
   601 session "HOL-SET_Protocol" in SET_Protocol = HOL +
   602   description {*
   603     Verification of the SET Protocol.
   604   *}
   605   options [document_graph]
   606   theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
   607   theories SET_Protocol
   608   files "document/root.tex"
   609 
   610 session "HOL-Matrix_LP" in Matrix_LP = HOL +
   611   description {*
   612     Two-dimensional matrices and linear programming.
   613   *}
   614   options [document_graph]
   615   theories Cplex
   616   files "document/root.tex"
   617 
   618 session "HOL-TLA" in TLA = HOL +
   619   description {*
   620     Lamport's Temporal Logic of Actions.
   621   *}
   622   options [document = false]
   623   theories TLA
   624 
   625 session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
   626   options [document = false]
   627   theories Inc
   628 
   629 session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
   630   options [document = false]
   631   theories DBuffer
   632 
   633 session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
   634   options [document = false]
   635   theories MemoryImplementation
   636 
   637 session "HOL-TPTP" in TPTP = HOL +
   638   description {*
   639     Author:     Jasmin Blanchette, TU Muenchen
   640     Author:     Nik Sultana, University of Cambridge
   641     Copyright   2011
   642 
   643     TPTP-related extensions.
   644   *}
   645   options [document = false]
   646   theories
   647     ATP_Theory_Export
   648     MaSh_Eval
   649     MaSh_Export
   650     TPTP_Interpret
   651     THF_Arith
   652   theories [proofs = 0]  (* FIXME !? *)
   653     ATP_Problem_Import
   654 
   655 session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +
   656   options [document_graph]
   657   theories
   658     Multivariate_Analysis
   659     Determinants
   660   files
   661     "document/root.tex"
   662 
   663 session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
   664   options [document_graph]
   665   theories [document = false]
   666     "~~/src/HOL/Library/Countable"
   667     "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
   668     "~~/src/HOL/Library/Permutation"
   669   theories
   670     Probability
   671     "ex/Dining_Cryptographers"
   672     "ex/Koepf_Duermuth_Countermeasure"
   673   files "document/root.tex"
   674 
   675 session "HOL-Nominal" (main) in Nominal = HOL +
   676   options [document = false]
   677   theories Nominal
   678 
   679 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
   680   options [timeout = 3600, condition = ISABELLE_POLYML, document = false]
   681   theories Nominal_Examples
   682   theories [quick_and_dirty] VC_Condition
   683 
   684 session "HOL-Cardinals-Base" in Cardinals = HOL +
   685   description {*
   686     Ordinals and Cardinals, Base Theories.
   687   *}
   688   options [document = false]
   689   theories Cardinal_Arithmetic
   690 
   691 session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" +
   692   description {*
   693     Ordinals and Cardinals, Full Theories.
   694   *}
   695   options [document = false]
   696   theories Cardinals
   697   files
   698     "document/intro.tex"
   699     "document/root.tex"
   700     "document/root.bib"
   701 
   702 session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-Base" +
   703   description {*
   704     Bounded Natural Functors for Datatypes.
   705   *}
   706   options [document = false]
   707   theories BNF_LFP
   708 
   709 session "HOL-BNF" in BNF = "HOL-Cardinals" +
   710   description {*
   711     Bounded Natural Functors for (Co)datatypes.
   712   *}
   713   options [document = false]
   714   theories BNF
   715 
   716 session "HOL-BNF-Examples" in "BNF/Examples" = "HOL-BNF" +
   717   description {*
   718     Examples for Bounded Natural Functors.
   719   *}
   720   options [document = false]
   721   theories
   722     Lambda_Term
   723     Process
   724     TreeFsetI
   725     "Derivation_Trees/Gram_Lang"
   726     "Derivation_Trees/Parallel"
   727     Koenig
   728   theories [condition = ISABELLE_FULL_TEST]
   729     Misc_Codata
   730     Misc_Data
   731 
   732 session "HOL-Word" (main) in Word = HOL +
   733   options [document_graph]
   734   theories Word
   735   files "document/root.bib" "document/root.tex"
   736 
   737 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   738   options [document = false]
   739   theories WordExamples
   740 
   741 session "HOL-Statespace" in Statespace = HOL +
   742   theories StateSpaceEx
   743   files "document/root.tex"
   744 
   745 session "HOL-NSA" in NSA = HOL +
   746   description {*
   747     Nonstandard analysis.
   748   *}
   749   options [document_graph]
   750   theories Hypercomplex
   751   files "document/root.tex"
   752 
   753 session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
   754   options [document = false]
   755   theories NSPrimes
   756 
   757 session "HOL-Mirabelle" in Mirabelle = HOL +
   758   options [document = false]
   759   theories Mirabelle_Test
   760 
   761 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   762   options [document = false, timeout = 60]
   763   theories Ex
   764 
   765 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
   766   options [document = false, quick_and_dirty]
   767   theories
   768     SMT_Examples
   769     SMT_Word_Examples
   770   theories [condition = ISABELLE_FULL_TEST]
   771     SMT_Tests
   772   files
   773     "SMT_Examples.certs"
   774     "SMT_Word_Examples.certs"
   775 
   776 session "HOL-Boogie" in "Boogie" = "HOL-Word" +
   777   options [document = false]
   778   theories Boogie
   779 
   780 session "HOL-Boogie-Examples" in "Boogie/Examples" = "HOL-Boogie" +
   781   options [document = false]
   782   theories
   783     Boogie_Max_Stepwise
   784     Boogie_Max
   785     Boogie_Dijkstra
   786     VCC_Max
   787   files
   788     "Boogie_Dijkstra.b2i"
   789     "Boogie_Dijkstra.certs"
   790     "Boogie_Max.b2i"
   791     "Boogie_Max.certs"
   792     "VCC_Max.b2i"
   793     "VCC_Max.certs"
   794 
   795 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   796   options [document = false]
   797   theories SPARK
   798 
   799 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   800   options [document = false]
   801   theories
   802     "Gcd/Greatest_Common_Divisor"
   803 
   804     "Liseq/Longest_Increasing_Subsequence"
   805 
   806     "RIPEMD-160/F"
   807     "RIPEMD-160/Hash"
   808     "RIPEMD-160/K_L"
   809     "RIPEMD-160/K_R"
   810     "RIPEMD-160/R_L"
   811     "RIPEMD-160/Round"
   812     "RIPEMD-160/R_R"
   813     "RIPEMD-160/S_L"
   814     "RIPEMD-160/S_R"
   815 
   816     "Sqrt/Sqrt"
   817   files
   818     "Gcd/greatest_common_divisor/g_c_d.fdl"
   819     "Gcd/greatest_common_divisor/g_c_d.rls"
   820     "Gcd/greatest_common_divisor/g_c_d.siv"
   821     "Liseq/liseq/liseq_length.fdl"
   822     "Liseq/liseq/liseq_length.rls"
   823     "Liseq/liseq/liseq_length.siv"
   824     "RIPEMD-160/rmd/f.fdl"
   825     "RIPEMD-160/rmd/f.rls"
   826     "RIPEMD-160/rmd/f.siv"
   827     "RIPEMD-160/rmd/hash.fdl"
   828     "RIPEMD-160/rmd/hash.rls"
   829     "RIPEMD-160/rmd/hash.siv"
   830     "RIPEMD-160/rmd/k_l.fdl"
   831     "RIPEMD-160/rmd/k_l.rls"
   832     "RIPEMD-160/rmd/k_l.siv"
   833     "RIPEMD-160/rmd/k_r.fdl"
   834     "RIPEMD-160/rmd/k_r.rls"
   835     "RIPEMD-160/rmd/k_r.siv"
   836     "RIPEMD-160/rmd/r_l.fdl"
   837     "RIPEMD-160/rmd/r_l.rls"
   838     "RIPEMD-160/rmd/r_l.siv"
   839     "RIPEMD-160/rmd/round.fdl"
   840     "RIPEMD-160/rmd/round.rls"
   841     "RIPEMD-160/rmd/round.siv"
   842     "RIPEMD-160/rmd/r_r.fdl"
   843     "RIPEMD-160/rmd/r_r.rls"
   844     "RIPEMD-160/rmd/r_r.siv"
   845     "RIPEMD-160/rmd/s_l.fdl"
   846     "RIPEMD-160/rmd/s_l.rls"
   847     "RIPEMD-160/rmd/s_l.siv"
   848     "RIPEMD-160/rmd/s_r.fdl"
   849     "RIPEMD-160/rmd/s_r.rls"
   850     "RIPEMD-160/rmd/s_r.siv"
   851 
   852 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   853   options [show_question_marks = false]
   854   theories
   855     Example_Verification
   856     VC_Principles
   857     Reference
   858     Complex_Types
   859   files
   860     "complex_types_app/initialize.fdl"
   861     "complex_types_app/initialize.rls"
   862     "complex_types_app/initialize.siv"
   863     "document/complex_types.ads"
   864     "document/complex_types_app.adb"
   865     "document/complex_types_app.ads"
   866     "document/Gcd.adb"
   867     "document/Gcd.ads"
   868     "document/intro.tex"
   869     "document/loop_invariant.adb"
   870     "document/loop_invariant.ads"
   871     "document/root.bib"
   872     "document/root.tex"
   873     "document/Simple_Gcd.adb"
   874     "document/Simple_Gcd.ads"
   875     "loop_invariant/proc1.fdl"
   876     "loop_invariant/proc1.rls"
   877     "loop_invariant/proc1.siv"
   878     "loop_invariant/proc2.fdl"
   879     "loop_invariant/proc2.rls"
   880     "loop_invariant/proc2.siv"
   881     "simple_greatest_common_divisor/g_c_d.fdl"
   882     "simple_greatest_common_divisor/g_c_d.rls"
   883     "simple_greatest_common_divisor/g_c_d.siv"
   884 
   885 session "HOL-Mutabelle" in Mutabelle = HOL +
   886   options [document = false]
   887   theories MutabelleExtra
   888 
   889 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
   890   options [document = false]
   891   theories
   892     Quickcheck_Examples
   893   (* FIXME
   894     Quickcheck_Lattice_Examples
   895     Completeness
   896     Quickcheck_Interfaces
   897     Hotel_Example *)
   898   theories [condition = ISABELLE_GHC]
   899     Quickcheck_Narrowing_Examples
   900 
   901 session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
   902   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
   903     Find_Unused_Assms_Examples
   904     Needham_Schroeder_No_Attacker_Example
   905     Needham_Schroeder_Guided_Attacker_Example
   906     Needham_Schroeder_Unguided_Attacker_Example
   907 
   908 session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
   909   description {*
   910     Author:     Cezary Kaliszyk and Christian Urban
   911   *}
   912   options [document = false]
   913   theories
   914     DList
   915     FSet
   916     Quotient_Int
   917     Quotient_Message
   918     Lift_FSet
   919     Lift_Set
   920     Lift_Fun
   921     Quotient_Rat
   922     Lift_DList
   923 
   924 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   925   options [document = false]
   926   theories
   927     Examples
   928     Predicate_Compile_Tests
   929     (* FIXME
   930     Predicate_Compile_Quickcheck_Examples  -- should be added again soon (since 21-Oct-2010) *)
   931     Specialisation_Examples
   932     (* FIXME since 21-Jul-2011
   933     Hotel_Example_Small_Generator
   934     IMP_1
   935     IMP_2
   936     IMP_3
   937     IMP_4 *)
   938   theories [condition = "ISABELLE_SWIPL"]  (* FIXME: *or* ISABELLE_YAP (??) *)
   939     Code_Prolog_Examples
   940     Context_Free_Grammar_Example
   941     Hotel_Example_Prolog
   942     Lambda_Example
   943     List_Examples
   944   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]  (* FIXME: *or* ISABELLE_YAP (??) *)
   945     Reg_Exp_Example
   946 
   947 session HOLCF (main) in HOLCF = HOL +
   948   description {*
   949     Author:     Franz Regensburger
   950     Author:     Brian Huffman
   951 
   952     HOLCF -- a semantic extension of HOL by the LCF logic.
   953   *}
   954   options [document_graph]
   955   theories [document = false]
   956     "~~/src/HOL/Library/Nat_Bijection"
   957     "~~/src/HOL/Library/Countable"
   958   theories
   959     Plain_HOLCF
   960     Fixrec
   961     HOLCF
   962   files "document/root.tex"
   963 
   964 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   965   theories
   966     Domain_ex
   967     Fixrec_ex
   968     New_Domain
   969   files "document/root.tex"
   970 
   971 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   972   options [document = false]
   973   theories HOLCF_Library
   974 
   975 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   976   description {*
   977     IMP -- A WHILE-language and its Semantics.
   978 
   979     This is the HOLCF-based denotational semantics of a simple WHILE-language.
   980   *}
   981   options [document = false]
   982   theories HoareEx
   983   files "document/root.tex"
   984 
   985 session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
   986   description {*
   987     Miscellaneous examples for HOLCF.
   988   *}
   989   options [document = false]
   990   theories
   991     Dnat
   992     Dagstuhl
   993     Focus_ex
   994     Fix2
   995     Hoare
   996     Concurrency_Monad
   997     Loop
   998     Powerdomain_ex
   999     Domain_Proofs
  1000     Letrec
  1001     Pattern_Match
  1002 
  1003 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
  1004   description {*
  1005     FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
  1006 
  1007     For introductions to FOCUS, see
  1008 
  1009     "The Design of Distributed Systems - An Introduction to FOCUS"
  1010     http://www4.in.tum.de/publ/html.php?e=2
  1011 
  1012     "Specification and Refinement of a Buffer of Length One"
  1013     http://www4.in.tum.de/publ/html.php?e=15
  1014 
  1015     "Specification and Development of Interactive Systems: Focus on Streams,
  1016     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
  1017   *}
  1018   options [document = false]
  1019   theories
  1020     Fstreams
  1021     FOCUS
  1022     Buffer_adm
  1023 
  1024 session IOA in "HOLCF/IOA" = HOLCF +
  1025   description {*
  1026     Author:     Olaf Mueller
  1027     Copyright   1997 TU München
  1028 
  1029     A formalization of I/O automata in HOLCF.
  1030 
  1031     The distribution contains simulation relations, temporal logic, and an
  1032     abstraction theory. Everything is based upon a domain-theoretic model of
  1033     finite and infinite sequences.
  1034   *}
  1035   options [document = false]
  1036   theories "meta_theory/Abstraction"
  1037 
  1038 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  1039   description {*
  1040     Author:     Olaf Mueller
  1041 
  1042     The Alternating Bit Protocol performed in I/O-Automata.
  1043   *}
  1044   options [document = false]
  1045   theories Correctness
  1046 
  1047 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
  1048   description {*
  1049     Author:     Tobias Nipkow & Konrad Slind
  1050 
  1051     A network transmission protocol, performed in the
  1052     I/O automata formalization by Olaf Mueller.
  1053   *}
  1054   options [document = false]
  1055   theories Correctness
  1056 
  1057 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
  1058   description {*
  1059     Author:     Olaf Mueller
  1060 
  1061     Memory storage case study.
  1062   *}
  1063   options [document = false]
  1064   theories Correctness
  1065 
  1066 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
  1067   description {*
  1068     Author:     Olaf Mueller
  1069   *}
  1070   options [document = false]
  1071   theories
  1072     TrivEx
  1073     TrivEx2
  1074 
  1075 session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
  1076   description {*
  1077     Some rather large datatype examples (from John Harrison).
  1078   *}
  1079   options [document = false]
  1080   theories [condition = ISABELLE_FULL_TEST, timing]
  1081     Brackin
  1082     Instructions
  1083     SML
  1084     Verilog
  1085 
  1086 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
  1087   description {*
  1088     Some benchmark on large record.
  1089   *}
  1090   options [document = false]
  1091   theories [condition = ISABELLE_FULL_TEST, timing]
  1092     Record_Benchmark
  1093