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