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