src/HOL/ROOT
author hoelzl
Tue Nov 05 09:44:57 2013 +0100 (2013-11-05)
changeset 54257 5c7a3b6b05a9
parent 54193 bc07627c5dcd
child 54429 be1bc181bcde
child 54447 019394de2b41
permissions -rw-r--r--
generalize SUP and INF to the syntactic type classes Sup and Inf
     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     RBT_Mapping
    47     RBT_Set
    48     (*legacy tools*)
    49     Refute
    50     Old_Recdef
    51   theories [condition = ISABELLE_FULL_TEST]
    52     Sum_of_Squares_Remote
    53   files "document/root.bib" "document/root.tex"
    54 
    55 session "HOL-Hahn_Banach" in Hahn_Banach = HOL +
    56   description {*
    57     Author:     Gertrud Bauer, TU Munich
    58 
    59     The Hahn-Banach theorem for real vector spaces.
    60 
    61     This is the proof of the Hahn-Banach theorem for real vectorspaces,
    62     following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach
    63     theorem is one of the fundamental theorems of functioal analysis. It is a
    64     conclusion of Zorn's lemma.
    65 
    66     Two different formaulations of the theorem are presented, one for general
    67     real vectorspaces and its application to normed vectorspaces.
    68 
    69     The theorem says, that every continous linearform, defined on arbitrary
    70     subspaces (not only one-dimensional subspaces), can be extended to a
    71     continous linearform on the whole vectorspace.
    72   *}
    73   options [document_graph]
    74   theories Hahn_Banach
    75   files "document/root.bib" "document/root.tex"
    76 
    77 session "HOL-Induct" in Induct = HOL +
    78   description {*
    79     Examples of (Co)Inductive Definitions.
    80 
    81     Comb proves the Church-Rosser theorem for combinators (see
    82     http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz).
    83 
    84     Mutil is the famous Mutilated Chess Board problem (see
    85     http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz).
    86 
    87     PropLog proves the completeness of a formalization of propositional logic
    88     (see
    89     HREF="http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz).
    90 
    91     Exp demonstrates the use of iterated inductive definitions to reason about
    92     mutually recursive relations.
    93   *}
    94   theories [quick_and_dirty]
    95     Common_Patterns
    96   theories
    97     QuoDataType
    98     QuoNestedDataType
    99     Term
   100     SList
   101     ABexp
   102     Tree
   103     Ordinals
   104     Sigma_Algebra
   105     Comb
   106     PropLog
   107     Com
   108   files "document/root.tex"
   109 
   110 session "HOL-IMP" in IMP = HOL +
   111   options [document_graph, document_variants=document]
   112   theories [document = false]
   113     "~~/src/HOL/ex/Interpretation_with_Defs"
   114     "~~/src/HOL/Library/While_Combinator"
   115     "~~/src/HOL/Library/Char_ord"
   116     "~~/src/HOL/Library/List_lexord"
   117     "~~/src/HOL/Library/Quotient_List"
   118     "~~/src/HOL/Library/Extended"
   119   theories
   120     BExp
   121     ASM
   122     Finite_Reachable
   123     Denotational
   124     Compiler2
   125     Poly_Types
   126     Sec_Typing
   127     Sec_TypingT
   128     Def_Init_Big
   129     Def_Init_Small
   130     Fold
   131     Live
   132     Live_True
   133     Hoare_Examples
   134     VCG
   135     Hoare_Total
   136     Collecting1
   137     Collecting_Examples
   138     Abs_Int_Tests
   139     Abs_Int1_parity
   140     Abs_Int1_const
   141     Abs_Int3
   142     "Abs_Int_ITP/Abs_Int1_parity_ITP"
   143     "Abs_Int_ITP/Abs_Int1_const_ITP"
   144     "Abs_Int_ITP/Abs_Int3_ITP"
   145     "Abs_Int_Den/Abs_Int_den2"
   146     Procs_Dyn_Vars_Dyn
   147     Procs_Stat_Vars_Dyn
   148     Procs_Stat_Vars_Stat
   149     C_like
   150     OO
   151   files "document/root.bib" "document/root.tex"
   152 
   153 session "HOL-IMPP" in IMPP = HOL +
   154   description {*
   155     Author:     David von Oheimb
   156     Copyright   1999 TUM
   157 
   158     IMPP -- An imperative language with procedures.
   159 
   160     This is an extension of IMP with local variables and mutually recursive
   161     procedures. For documentation see "Hoare Logic for Mutual Recursion and
   162     Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
   163   *}
   164   options [document = false]
   165   theories EvenOdd
   166 
   167 session "HOL-Import" in Import = HOL +
   168   options [document_graph]
   169   theories HOL_Light_Maps
   170   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
   171 
   172 session "HOL-Number_Theory" in Number_Theory = HOL +
   173   options [document = false]
   174   theories Number_Theory
   175 
   176 session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
   177   description {*
   178     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
   179     Theorem, Wilson's Theorem, Quadratic Reciprocity.
   180   *}
   181   options [document_graph]
   182   theories [document = false]
   183     "~~/src/HOL/Library/Infinite_Set"
   184     "~~/src/HOL/Library/Permutation"
   185   theories
   186     Fib
   187     Factorization
   188     Chinese
   189     WilsonRuss
   190     WilsonBij
   191     Quadratic_Reciprocity
   192     Primes
   193     Pocklington
   194   files "document/root.tex"
   195 
   196 session "HOL-Hoare" in Hoare = HOL +
   197   description {*
   198     Verification of imperative programs (verification conditions are generated
   199     automatically from pre/post conditions and loop invariants).
   200   *}
   201 
   202   theories Hoare
   203   files "document/root.bib" "document/root.tex"
   204 
   205 session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL +
   206   description {*
   207     Verification of shared-variable imperative programs a la Owicki-Gries.
   208     (verification conditions are generated automatically).
   209   *}
   210   options [document_graph]
   211   theories Hoare_Parallel
   212   files "document/root.bib" "document/root.tex"
   213 
   214 session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
   215   options [document = false, document_graph = false, browser_info = false]
   216   theories
   217     Generate
   218     Generate_Binary_Nat
   219     Generate_Target_Nat
   220     Generate_Efficient_Datastructures
   221     Generate_Pretty_Char
   222 
   223 session "HOL-Metis_Examples" in Metis_Examples = HOL +
   224   description {*
   225     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   226     Author:     Jasmin Blanchette, TU Muenchen
   227 
   228     Testing Metis and Sledgehammer.
   229   *}
   230   options [timeout = 3600, document = false]
   231   theories
   232     Abstraction
   233     Big_O
   234     Binary_Tree
   235     Clausification
   236     Message
   237     Proxies
   238     Tarski
   239     Trans_Closure
   240     Sets
   241 
   242 session "HOL-BNF-Nitpick_Examples" in Nitpick_Examples = "HOL-BNF" +
   243   description {*
   244     Author:     Jasmin Blanchette, TU Muenchen
   245     Copyright   2009
   246   *}
   247   options [document = false]
   248   theories [quick_and_dirty] Nitpick_Examples
   249 
   250 session "HOL-Algebra" (main) in Algebra = HOL +
   251   description {*
   252     Author: Clemens Ballarin, started 24 September 1999
   253 
   254     The Isabelle Algebraic Library.
   255   *}
   256   options [document_graph]
   257   theories [document = false]
   258     (* Preliminaries from set and number theory *)
   259     "~~/src/HOL/Library/FuncSet"
   260     "~~/src/HOL/Old_Number_Theory/Primes"
   261     "~~/src/HOL/Library/Binomial"
   262     "~~/src/HOL/Library/Permutation"
   263   theories
   264     (*** New development, based on explicit structures ***)
   265     (* Groups *)
   266     FiniteProduct        (* Product operator for commutative groups *)
   267     Sylow                (* Sylow's theorem *)
   268     Bij                  (* Automorphism Groups *)
   269 
   270     (* Rings *)
   271     Divisibility         (* Rings *)
   272     IntRing              (* Ideals and residue classes *)
   273     UnivPoly             (* Polynomials *)
   274   files "document/root.bib" "document/root.tex"
   275 
   276 session "HOL-Auth" in Auth = HOL +
   277   description {*
   278     A new approach to verifying authentication protocols.
   279   *}
   280   options [document_graph]
   281   theories
   282     Auth_Shared
   283     Auth_Public
   284     "Smartcard/Auth_Smartcard"
   285     "Guard/Auth_Guard_Shared"
   286     "Guard/Auth_Guard_Public"
   287   files "document/root.tex"
   288 
   289 session "HOL-UNITY" in UNITY = "HOL-Auth" +
   290   description {*
   291     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   292     Copyright   1998  University of Cambridge
   293 
   294     Verifying security protocols using Chandy and Misra's UNITY formalism.
   295   *}
   296   options [document_graph]
   297   theories
   298     (*Basic meta-theory*)
   299     "UNITY_Main"
   300 
   301     (*Simple examples: no composition*)
   302     "Simple/Deadlock"
   303     "Simple/Common"
   304     "Simple/Network"
   305     "Simple/Token"
   306     "Simple/Channel"
   307     "Simple/Lift"
   308     "Simple/Mutex"
   309     "Simple/Reach"
   310     "Simple/Reachability"
   311 
   312     (*Verifying security protocols using UNITY*)
   313     "Simple/NSP_Bad"
   314 
   315     (*Example of composition*)
   316     "Comp/Handshake"
   317 
   318     (*Universal properties examples*)
   319     "Comp/Counter"
   320     "Comp/Counterc"
   321     "Comp/Priority"
   322 
   323     "Comp/TimerArray"
   324     "Comp/Progress"
   325 
   326     "Comp/Alloc"
   327     "Comp/AllocImpl"
   328     "Comp/Client"
   329 
   330     (*obsolete*)
   331     "ELT"
   332   files "document/root.tex"
   333 
   334 session "HOL-Unix" in Unix = HOL +
   335   options [print_mode = "no_brackets,no_type_brackets"]
   336   theories Unix
   337   files "document/root.bib" "document/root.tex"
   338 
   339 session "HOL-ZF" in ZF = HOL +
   340   theories MainZF Games
   341   files "document/root.tex"
   342 
   343 session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
   344   options [document_graph, print_mode = "iff,no_brackets"]
   345   theories [document = false]
   346     "~~/src/HOL/Library/Countable"
   347     "~~/src/HOL/Library/Monad_Syntax"
   348     "~~/src/HOL/Library/LaTeXsugar"
   349   theories Imperative_HOL_ex
   350   files "document/root.bib" "document/root.tex"
   351 
   352 session "HOL-Decision_Procs" in Decision_Procs = HOL +
   353   description {*
   354     Various decision procedures, typically involving reflection.
   355   *}
   356   options [condition = ISABELLE_POLYML, document = false]
   357   theories Decision_Procs
   358 
   359 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
   360   options [document = false, parallel_proofs = 0]
   361   theories
   362     Hilbert_Classical
   363     XML_Data
   364 
   365 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
   366   description {*
   367     Examples for program extraction in Higher-Order Logic.
   368   *}
   369   options [condition = ISABELLE_POLYML, parallel_proofs = 0]
   370   theories [document = false]
   371     "~~/src/HOL/Library/Code_Target_Numeral"
   372     "~~/src/HOL/Library/Monad_Syntax"
   373     "~~/src/HOL/Number_Theory/Primes"
   374     "~~/src/HOL/Number_Theory/UniqueFactorization"
   375     "~~/src/HOL/Library/State_Monad"
   376   theories
   377     Greatest_Common_Divisor
   378     Warshall
   379     Higman_Extraction
   380     Pigeonhole
   381     Euclid
   382   files "document/root.bib" "document/root.tex"
   383 
   384 session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +
   385   description {*
   386     Lambda Calculus in de Bruijn's Notation.
   387 
   388     This session defines lambda-calculus terms with de Bruijn indixes and
   389     proves confluence of beta, eta and beta+eta.
   390 
   391     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
   392     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
   393   *}
   394   options [document_graph, print_mode = "no_brackets", parallel_proofs = 0]
   395   theories [document = false]
   396     "~~/src/HOL/Library/Code_Target_Int"
   397   theories
   398     Eta
   399     StrongNorm
   400     Standardization
   401     WeakNorm
   402   files "document/root.bib" "document/root.tex"
   403 
   404 session "HOL-Prolog" in Prolog = HOL +
   405   description {*
   406     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
   407 
   408     A bare-bones implementation of Lambda-Prolog.
   409 
   410     This is a simple exploratory implementation of Lambda-Prolog in HOL,
   411     including some minimal examples (in Test.thy) and a more typical example of
   412     a little functional language and its type system.
   413   *}
   414   options [document = false]
   415   theories Test Type
   416 
   417 session "HOL-MicroJava" in MicroJava = HOL +
   418   description {*
   419     Formalization of a fragment of Java, together with a corresponding virtual
   420     machine and a specification of its bytecode verifier and a lightweight
   421     bytecode verifier, including proofs of type-safety.
   422   *}
   423   options [document_graph]
   424   theories [document = false] "~~/src/HOL/Library/While_Combinator"
   425   theories MicroJava
   426   files
   427     "document/introduction.tex"
   428     "document/root.bib"
   429     "document/root.tex"
   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     Higher_Order_Logic
   508     Abstract_NAT
   509     Guess
   510     Fundefs
   511     Induction_Schema
   512     LocaleTest2
   513     Records
   514     While_Combinator_Example
   515     MonoidGroup
   516     BinEx
   517     Hex_Bin_Examples
   518     Antiquote
   519     Multiquote
   520     PER
   521     NatSum
   522     ThreeDivides
   523     Intuitionistic
   524     CTL
   525     Arith_Examples
   526     BT
   527     Tree23
   528     MergeSort
   529     Lagrange
   530     Groebner_Examples
   531     MT
   532     Unification
   533     Primrec
   534     Tarski
   535     Classical
   536     Set_Theory
   537     Termination
   538     Coherent
   539     PresburgerEx
   540     Reflection_Examples
   541     Sqrt
   542     Sqrt_Script
   543     Transfer_Ex
   544     Transfer_Int_Nat
   545     HarmonicSeries
   546     Refute_Examples
   547     Execute_Choice
   548     Summation
   549     Gauge_Integration
   550     Dedekind_Real
   551     Quicksort
   552     Birthday_Paradox
   553     List_to_Set_Comprehension_Examples
   554     Seq
   555     Simproc_Tests
   556     Executable_Relation
   557     FinFunPred
   558     Set_Comprehension_Pointfree_Tests
   559     Parallel_Example
   560     IArray_Examples
   561     SVC_Oracle
   562     Simps_Case_Conv_Examples
   563     ML
   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
   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_Codatatype
   735     Misc_Datatype
   736     Misc_Primcorec
   737     Misc_Primrec
   738 
   739 session "HOL-Word" (main) in Word = HOL +
   740   options [document_graph]
   741   theories Word
   742   files "document/root.bib" "document/root.tex"
   743 
   744 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   745   options [document = false]
   746   theories WordExamples
   747 
   748 session "HOL-Statespace" in Statespace = HOL +
   749   theories [skip_proofs = false]
   750     StateSpaceEx
   751   files "document/root.tex"
   752 
   753 session "HOL-NSA" in NSA = HOL +
   754   description {*
   755     Nonstandard analysis.
   756   *}
   757   options [document_graph]
   758   theories Hypercomplex
   759   files "document/root.tex"
   760 
   761 session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
   762   options [document = false]
   763   theories NSPrimes
   764 
   765 session "HOL-Mirabelle" in Mirabelle = HOL +
   766   options [document = false]
   767   theories Mirabelle_Test
   768 
   769 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   770   options [document = false, timeout = 60]
   771   theories Ex
   772 
   773 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
   774   options [document = false, quick_and_dirty]
   775   theories
   776     Boogie
   777     SMT_Examples
   778     SMT_Word_Examples
   779   theories [condition = ISABELLE_FULL_TEST]
   780     SMT_Tests
   781   files
   782     "Boogie_Dijkstra.b2i"
   783     "Boogie_Dijkstra.certs"
   784     "Boogie_Max.b2i"
   785     "Boogie_Max.certs"
   786     "SMT_Examples.certs"
   787     "SMT_Word_Examples.certs"
   788     "VCC_Max.b2i"
   789     "VCC_Max.certs"
   790 
   791 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   792   options [document = false]
   793   theories SPARK
   794 
   795 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   796   options [document = false]
   797   theories
   798     "Gcd/Greatest_Common_Divisor"
   799 
   800     "Liseq/Longest_Increasing_Subsequence"
   801 
   802     "RIPEMD-160/F"
   803     "RIPEMD-160/Hash"
   804     "RIPEMD-160/K_L"
   805     "RIPEMD-160/K_R"
   806     "RIPEMD-160/R_L"
   807     "RIPEMD-160/Round"
   808     "RIPEMD-160/R_R"
   809     "RIPEMD-160/S_L"
   810     "RIPEMD-160/S_R"
   811 
   812     "Sqrt/Sqrt"
   813   files
   814     "Gcd/greatest_common_divisor/g_c_d.fdl"
   815     "Gcd/greatest_common_divisor/g_c_d.rls"
   816     "Gcd/greatest_common_divisor/g_c_d.siv"
   817     "Liseq/liseq/liseq_length.fdl"
   818     "Liseq/liseq/liseq_length.rls"
   819     "Liseq/liseq/liseq_length.siv"
   820     "RIPEMD-160/rmd/f.fdl"
   821     "RIPEMD-160/rmd/f.rls"
   822     "RIPEMD-160/rmd/f.siv"
   823     "RIPEMD-160/rmd/hash.fdl"
   824     "RIPEMD-160/rmd/hash.rls"
   825     "RIPEMD-160/rmd/hash.siv"
   826     "RIPEMD-160/rmd/k_l.fdl"
   827     "RIPEMD-160/rmd/k_l.rls"
   828     "RIPEMD-160/rmd/k_l.siv"
   829     "RIPEMD-160/rmd/k_r.fdl"
   830     "RIPEMD-160/rmd/k_r.rls"
   831     "RIPEMD-160/rmd/k_r.siv"
   832     "RIPEMD-160/rmd/r_l.fdl"
   833     "RIPEMD-160/rmd/r_l.rls"
   834     "RIPEMD-160/rmd/r_l.siv"
   835     "RIPEMD-160/rmd/round.fdl"
   836     "RIPEMD-160/rmd/round.rls"
   837     "RIPEMD-160/rmd/round.siv"
   838     "RIPEMD-160/rmd/r_r.fdl"
   839     "RIPEMD-160/rmd/r_r.rls"
   840     "RIPEMD-160/rmd/r_r.siv"
   841     "RIPEMD-160/rmd/s_l.fdl"
   842     "RIPEMD-160/rmd/s_l.rls"
   843     "RIPEMD-160/rmd/s_l.siv"
   844     "RIPEMD-160/rmd/s_r.fdl"
   845     "RIPEMD-160/rmd/s_r.rls"
   846     "RIPEMD-160/rmd/s_r.siv"
   847 
   848 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   849   options [show_question_marks = false]
   850   theories
   851     Example_Verification
   852     VC_Principles
   853     Reference
   854     Complex_Types
   855   files
   856     "complex_types_app/initialize.fdl"
   857     "complex_types_app/initialize.rls"
   858     "complex_types_app/initialize.siv"
   859     "document/complex_types.ads"
   860     "document/complex_types_app.adb"
   861     "document/complex_types_app.ads"
   862     "document/Gcd.adb"
   863     "document/Gcd.ads"
   864     "document/intro.tex"
   865     "document/loop_invariant.adb"
   866     "document/loop_invariant.ads"
   867     "document/root.bib"
   868     "document/root.tex"
   869     "document/Simple_Gcd.adb"
   870     "document/Simple_Gcd.ads"
   871     "loop_invariant/proc1.fdl"
   872     "loop_invariant/proc1.rls"
   873     "loop_invariant/proc1.siv"
   874     "loop_invariant/proc2.fdl"
   875     "loop_invariant/proc2.rls"
   876     "loop_invariant/proc2.siv"
   877     "simple_greatest_common_divisor/g_c_d.fdl"
   878     "simple_greatest_common_divisor/g_c_d.rls"
   879     "simple_greatest_common_divisor/g_c_d.siv"
   880 
   881 session "HOL-Mutabelle" in Mutabelle = HOL +
   882   options [document = false]
   883   theories MutabelleExtra
   884 
   885 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
   886   options [document = false]
   887   theories
   888     Quickcheck_Examples
   889   (* FIXME
   890     Quickcheck_Lattice_Examples
   891     Completeness
   892     Quickcheck_Interfaces
   893     Hotel_Example *)
   894   theories [condition = ISABELLE_GHC]
   895     Quickcheck_Narrowing_Examples
   896 
   897 session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
   898   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
   899     Find_Unused_Assms_Examples
   900     Needham_Schroeder_No_Attacker_Example
   901     Needham_Schroeder_Guided_Attacker_Example
   902     Needham_Schroeder_Unguided_Attacker_Example
   903 
   904 session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
   905   description {*
   906     Author:     Cezary Kaliszyk and Christian Urban
   907   *}
   908   options [document = false]
   909   theories
   910     DList
   911     FSet
   912     Quotient_Int
   913     Quotient_Message
   914     Lift_FSet
   915     Lift_Set
   916     Lift_Fun
   917     Quotient_Rat
   918     Lift_DList
   919     Int_Pow
   920 
   921 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   922   options [document = false]
   923   theories
   924     Examples
   925     Predicate_Compile_Tests
   926     (* FIXME
   927     Predicate_Compile_Quickcheck_Examples  -- should be added again soon (since 21-Oct-2010) *)
   928     Specialisation_Examples
   929     (* FIXME since 21-Jul-2011
   930     Hotel_Example_Small_Generator
   931     IMP_1
   932     IMP_2
   933     IMP_3
   934     IMP_4 *)
   935   theories [condition = "ISABELLE_SWIPL"]  (* FIXME: *or* ISABELLE_YAP (??) *)
   936     Code_Prolog_Examples
   937     Context_Free_Grammar_Example
   938     Hotel_Example_Prolog
   939     Lambda_Example
   940     List_Examples
   941   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]  (* FIXME: *or* ISABELLE_YAP (??) *)
   942     Reg_Exp_Example
   943 
   944 session HOLCF (main) in HOLCF = HOL +
   945   description {*
   946     Author:     Franz Regensburger
   947     Author:     Brian Huffman
   948 
   949     HOLCF -- a semantic extension of HOL by the LCF logic.
   950   *}
   951   options [document_graph]
   952   theories [document = false]
   953     "~~/src/HOL/Library/Nat_Bijection"
   954     "~~/src/HOL/Library/Countable"
   955   theories
   956     Plain_HOLCF
   957     Fixrec
   958     HOLCF
   959   files "document/root.tex"
   960 
   961 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   962   theories
   963     Domain_ex
   964     Fixrec_ex
   965     New_Domain
   966   files "document/root.tex"
   967 
   968 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   969   options [document = false]
   970   theories HOLCF_Library
   971 
   972 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   973   description {*
   974     IMP -- A WHILE-language and its Semantics.
   975 
   976     This is the HOLCF-based denotational semantics of a simple WHILE-language.
   977   *}
   978   options [document = false]
   979   theories HoareEx
   980   files "document/root.tex"
   981 
   982 session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
   983   description {*
   984     Miscellaneous examples for HOLCF.
   985   *}
   986   options [document = false]
   987   theories
   988     Dnat
   989     Dagstuhl
   990     Focus_ex
   991     Fix2
   992     Hoare
   993     Concurrency_Monad
   994     Loop
   995     Powerdomain_ex
   996     Domain_Proofs
   997     Letrec
   998     Pattern_Match
   999 
  1000 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
  1001   description {*
  1002     FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
  1003 
  1004     For introductions to FOCUS, see
  1005 
  1006     "The Design of Distributed Systems - An Introduction to FOCUS"
  1007     http://www4.in.tum.de/publ/html.php?e=2
  1008 
  1009     "Specification and Refinement of a Buffer of Length One"
  1010     http://www4.in.tum.de/publ/html.php?e=15
  1011 
  1012     "Specification and Development of Interactive Systems: Focus on Streams,
  1013     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
  1014   *}
  1015   options [document = false]
  1016   theories
  1017     Fstreams
  1018     FOCUS
  1019     Buffer_adm
  1020 
  1021 session IOA in "HOLCF/IOA" = HOLCF +
  1022   description {*
  1023     Author:     Olaf Mueller
  1024     Copyright   1997 TU München
  1025 
  1026     A formalization of I/O automata in HOLCF.
  1027 
  1028     The distribution contains simulation relations, temporal logic, and an
  1029     abstraction theory. Everything is based upon a domain-theoretic model of
  1030     finite and infinite sequences.
  1031   *}
  1032   options [document = false]
  1033   theories "meta_theory/Abstraction"
  1034 
  1035 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  1036   description {*
  1037     Author:     Olaf Mueller
  1038 
  1039     The Alternating Bit Protocol performed in I/O-Automata.
  1040   *}
  1041   options [document = false]
  1042   theories Correctness
  1043 
  1044 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
  1045   description {*
  1046     Author:     Tobias Nipkow & Konrad Slind
  1047 
  1048     A network transmission protocol, performed in the
  1049     I/O automata formalization by Olaf Mueller.
  1050   *}
  1051   options [document = false]
  1052   theories Correctness
  1053 
  1054 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
  1055   description {*
  1056     Author:     Olaf Mueller
  1057 
  1058     Memory storage case study.
  1059   *}
  1060   options [document = false]
  1061   theories Correctness
  1062 
  1063 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
  1064   description {*
  1065     Author:     Olaf Mueller
  1066   *}
  1067   options [document = false]
  1068   theories
  1069     TrivEx
  1070     TrivEx2
  1071 
  1072 session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
  1073   description {*
  1074     Some rather large datatype examples (from John Harrison).
  1075   *}
  1076   options [document = false]
  1077   theories [condition = ISABELLE_FULL_TEST, timing]
  1078     Brackin
  1079     Instructions
  1080     SML
  1081     Verilog
  1082 
  1083 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
  1084   description {*
  1085     Some benchmark on large record.
  1086   *}
  1087   options [document = false]
  1088   theories [condition = ISABELLE_FULL_TEST, timing]
  1089     Record_Benchmark
  1090