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