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