src/HOL/ROOT
author wenzelm
Fri May 31 11:56:48 2013 +0200 (2013-05-31)
changeset 52277 2bbeab01c0ea
parent 52269 d867812da48b
child 52282 c79a3e15779e
permissions -rw-r--r--
make SML/NJ partially happy;
     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     VCG
   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-Spec_Check" in Spec_Check = HOL +
   744   theories
   745     Spec_Check
   746   theories [condition = ISABELLE_POLYML]
   747     Examples
   748 
   749 session "HOL-Statespace" in Statespace = HOL +
   750   theories [skip_proofs = false]
   751     StateSpaceEx
   752   files "document/root.tex"
   753 
   754 session "HOL-NSA" in NSA = HOL +
   755   description {*
   756     Nonstandard analysis.
   757   *}
   758   options [document_graph]
   759   theories Hypercomplex
   760   files "document/root.tex"
   761 
   762 session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
   763   options [document = false]
   764   theories NSPrimes
   765 
   766 session "HOL-Mirabelle" in Mirabelle = HOL +
   767   options [document = false]
   768   theories Mirabelle_Test
   769 
   770 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   771   options [document = false, timeout = 60]
   772   theories Ex
   773 
   774 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
   775   options [document = false, quick_and_dirty]
   776   theories
   777     SMT_Examples
   778     SMT_Word_Examples
   779   theories [condition = ISABELLE_FULL_TEST]
   780     SMT_Tests
   781   files
   782     "SMT_Examples.certs"
   783     "SMT_Word_Examples.certs"
   784 
   785 session "HOL-Boogie" in "Boogie" = "HOL-Word" +
   786   options [document = false]
   787   theories Boogie
   788 
   789 session "HOL-Boogie-Examples" in "Boogie/Examples" = "HOL-Boogie" +
   790   options [document = false]
   791   theories
   792     Boogie_Max_Stepwise
   793     Boogie_Max
   794     Boogie_Dijkstra
   795     VCC_Max
   796   files
   797     "Boogie_Dijkstra.b2i"
   798     "Boogie_Dijkstra.certs"
   799     "Boogie_Max.b2i"
   800     "Boogie_Max.certs"
   801     "VCC_Max.b2i"
   802     "VCC_Max.certs"
   803 
   804 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   805   options [document = false]
   806   theories SPARK
   807 
   808 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   809   options [document = false]
   810   theories
   811     "Gcd/Greatest_Common_Divisor"
   812 
   813     "Liseq/Longest_Increasing_Subsequence"
   814 
   815     "RIPEMD-160/F"
   816     "RIPEMD-160/Hash"
   817     "RIPEMD-160/K_L"
   818     "RIPEMD-160/K_R"
   819     "RIPEMD-160/R_L"
   820     "RIPEMD-160/Round"
   821     "RIPEMD-160/R_R"
   822     "RIPEMD-160/S_L"
   823     "RIPEMD-160/S_R"
   824 
   825     "Sqrt/Sqrt"
   826   files
   827     "Gcd/greatest_common_divisor/g_c_d.fdl"
   828     "Gcd/greatest_common_divisor/g_c_d.rls"
   829     "Gcd/greatest_common_divisor/g_c_d.siv"
   830     "Liseq/liseq/liseq_length.fdl"
   831     "Liseq/liseq/liseq_length.rls"
   832     "Liseq/liseq/liseq_length.siv"
   833     "RIPEMD-160/rmd/f.fdl"
   834     "RIPEMD-160/rmd/f.rls"
   835     "RIPEMD-160/rmd/f.siv"
   836     "RIPEMD-160/rmd/hash.fdl"
   837     "RIPEMD-160/rmd/hash.rls"
   838     "RIPEMD-160/rmd/hash.siv"
   839     "RIPEMD-160/rmd/k_l.fdl"
   840     "RIPEMD-160/rmd/k_l.rls"
   841     "RIPEMD-160/rmd/k_l.siv"
   842     "RIPEMD-160/rmd/k_r.fdl"
   843     "RIPEMD-160/rmd/k_r.rls"
   844     "RIPEMD-160/rmd/k_r.siv"
   845     "RIPEMD-160/rmd/r_l.fdl"
   846     "RIPEMD-160/rmd/r_l.rls"
   847     "RIPEMD-160/rmd/r_l.siv"
   848     "RIPEMD-160/rmd/round.fdl"
   849     "RIPEMD-160/rmd/round.rls"
   850     "RIPEMD-160/rmd/round.siv"
   851     "RIPEMD-160/rmd/r_r.fdl"
   852     "RIPEMD-160/rmd/r_r.rls"
   853     "RIPEMD-160/rmd/r_r.siv"
   854     "RIPEMD-160/rmd/s_l.fdl"
   855     "RIPEMD-160/rmd/s_l.rls"
   856     "RIPEMD-160/rmd/s_l.siv"
   857     "RIPEMD-160/rmd/s_r.fdl"
   858     "RIPEMD-160/rmd/s_r.rls"
   859     "RIPEMD-160/rmd/s_r.siv"
   860 
   861 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   862   options [show_question_marks = false]
   863   theories
   864     Example_Verification
   865     VC_Principles
   866     Reference
   867     Complex_Types
   868   files
   869     "complex_types_app/initialize.fdl"
   870     "complex_types_app/initialize.rls"
   871     "complex_types_app/initialize.siv"
   872     "document/complex_types.ads"
   873     "document/complex_types_app.adb"
   874     "document/complex_types_app.ads"
   875     "document/Gcd.adb"
   876     "document/Gcd.ads"
   877     "document/intro.tex"
   878     "document/loop_invariant.adb"
   879     "document/loop_invariant.ads"
   880     "document/root.bib"
   881     "document/root.tex"
   882     "document/Simple_Gcd.adb"
   883     "document/Simple_Gcd.ads"
   884     "loop_invariant/proc1.fdl"
   885     "loop_invariant/proc1.rls"
   886     "loop_invariant/proc1.siv"
   887     "loop_invariant/proc2.fdl"
   888     "loop_invariant/proc2.rls"
   889     "loop_invariant/proc2.siv"
   890     "simple_greatest_common_divisor/g_c_d.fdl"
   891     "simple_greatest_common_divisor/g_c_d.rls"
   892     "simple_greatest_common_divisor/g_c_d.siv"
   893 
   894 session "HOL-Mutabelle" in Mutabelle = HOL +
   895   options [document = false]
   896   theories MutabelleExtra
   897 
   898 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
   899   options [document = false]
   900   theories
   901     Quickcheck_Examples
   902   (* FIXME
   903     Quickcheck_Lattice_Examples
   904     Completeness
   905     Quickcheck_Interfaces
   906     Hotel_Example *)
   907   theories [condition = ISABELLE_GHC]
   908     Quickcheck_Narrowing_Examples
   909 
   910 session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
   911   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
   912     Find_Unused_Assms_Examples
   913     Needham_Schroeder_No_Attacker_Example
   914     Needham_Schroeder_Guided_Attacker_Example
   915     Needham_Schroeder_Unguided_Attacker_Example
   916 
   917 session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
   918   description {*
   919     Author:     Cezary Kaliszyk and Christian Urban
   920   *}
   921   options [document = false]
   922   theories
   923     DList
   924     FSet
   925     Quotient_Int
   926     Quotient_Message
   927     Lift_FSet
   928     Lift_Set
   929     Lift_Fun
   930     Quotient_Rat
   931     Lift_DList
   932 
   933 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   934   options [document = false]
   935   theories
   936     Examples
   937     Predicate_Compile_Tests
   938     (* FIXME
   939     Predicate_Compile_Quickcheck_Examples  -- should be added again soon (since 21-Oct-2010) *)
   940     Specialisation_Examples
   941     (* FIXME since 21-Jul-2011
   942     Hotel_Example_Small_Generator
   943     IMP_1
   944     IMP_2
   945     IMP_3
   946     IMP_4 *)
   947   theories [condition = "ISABELLE_SWIPL"]  (* FIXME: *or* ISABELLE_YAP (??) *)
   948     Code_Prolog_Examples
   949     Context_Free_Grammar_Example
   950     Hotel_Example_Prolog
   951     Lambda_Example
   952     List_Examples
   953   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]  (* FIXME: *or* ISABELLE_YAP (??) *)
   954     Reg_Exp_Example
   955 
   956 session HOLCF (main) in HOLCF = HOL +
   957   description {*
   958     Author:     Franz Regensburger
   959     Author:     Brian Huffman
   960 
   961     HOLCF -- a semantic extension of HOL by the LCF logic.
   962   *}
   963   options [document_graph]
   964   theories [document = false]
   965     "~~/src/HOL/Library/Nat_Bijection"
   966     "~~/src/HOL/Library/Countable"
   967   theories
   968     Plain_HOLCF
   969     Fixrec
   970     HOLCF
   971   files "document/root.tex"
   972 
   973 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   974   theories
   975     Domain_ex
   976     Fixrec_ex
   977     New_Domain
   978   files "document/root.tex"
   979 
   980 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   981   options [document = false]
   982   theories HOLCF_Library
   983 
   984 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   985   description {*
   986     IMP -- A WHILE-language and its Semantics.
   987 
   988     This is the HOLCF-based denotational semantics of a simple WHILE-language.
   989   *}
   990   options [document = false]
   991   theories HoareEx
   992   files "document/root.tex"
   993 
   994 session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
   995   description {*
   996     Miscellaneous examples for HOLCF.
   997   *}
   998   options [document = false]
   999   theories
  1000     Dnat
  1001     Dagstuhl
  1002     Focus_ex
  1003     Fix2
  1004     Hoare
  1005     Concurrency_Monad
  1006     Loop
  1007     Powerdomain_ex
  1008     Domain_Proofs
  1009     Letrec
  1010     Pattern_Match
  1011 
  1012 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
  1013   description {*
  1014     FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
  1015 
  1016     For introductions to FOCUS, see
  1017 
  1018     "The Design of Distributed Systems - An Introduction to FOCUS"
  1019     http://www4.in.tum.de/publ/html.php?e=2
  1020 
  1021     "Specification and Refinement of a Buffer of Length One"
  1022     http://www4.in.tum.de/publ/html.php?e=15
  1023 
  1024     "Specification and Development of Interactive Systems: Focus on Streams,
  1025     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
  1026   *}
  1027   options [document = false]
  1028   theories
  1029     Fstreams
  1030     FOCUS
  1031     Buffer_adm
  1032 
  1033 session IOA in "HOLCF/IOA" = HOLCF +
  1034   description {*
  1035     Author:     Olaf Mueller
  1036     Copyright   1997 TU München
  1037 
  1038     A formalization of I/O automata in HOLCF.
  1039 
  1040     The distribution contains simulation relations, temporal logic, and an
  1041     abstraction theory. Everything is based upon a domain-theoretic model of
  1042     finite and infinite sequences.
  1043   *}
  1044   options [document = false]
  1045   theories "meta_theory/Abstraction"
  1046 
  1047 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  1048   description {*
  1049     Author:     Olaf Mueller
  1050 
  1051     The Alternating Bit Protocol performed in I/O-Automata.
  1052   *}
  1053   options [document = false]
  1054   theories Correctness
  1055 
  1056 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
  1057   description {*
  1058     Author:     Tobias Nipkow & Konrad Slind
  1059 
  1060     A network transmission protocol, performed in the
  1061     I/O automata formalization by Olaf Mueller.
  1062   *}
  1063   options [document = false]
  1064   theories Correctness
  1065 
  1066 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
  1067   description {*
  1068     Author:     Olaf Mueller
  1069 
  1070     Memory storage case study.
  1071   *}
  1072   options [document = false]
  1073   theories Correctness
  1074 
  1075 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
  1076   description {*
  1077     Author:     Olaf Mueller
  1078   *}
  1079   options [document = false]
  1080   theories
  1081     TrivEx
  1082     TrivEx2
  1083 
  1084 session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
  1085   description {*
  1086     Some rather large datatype examples (from John Harrison).
  1087   *}
  1088   options [document = false]
  1089   theories [condition = ISABELLE_FULL_TEST, timing]
  1090     Brackin
  1091     Instructions
  1092     SML
  1093     Verilog
  1094 
  1095 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
  1096   description {*
  1097     Some benchmark on large record.
  1098   *}
  1099   options [document = false]
  1100   theories [condition = ISABELLE_FULL_TEST, timing]
  1101     Record_Benchmark
  1102