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