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