src/HOL/ROOT
author sultana
Wed Feb 19 15:57:02 2014 +0000 (2014-02-19)
changeset 55596 928b9f677165
parent 55450 9eddc17749f7
child 55601 b7f4da504b75
permissions -rw-r--r--
reconstruction framework for LEO-II's TPTP proofs;
     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/HOL/ex/Interpretation_with_Defs"
   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, 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     Number_Theory
   187   files
   188     "document/root.tex"
   189 
   190 session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
   191   description {*
   192     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
   193     Theorem, Wilson's Theorem, Quadratic Reciprocity.
   194   *}
   195   options [document_graph]
   196   theories [document = false]
   197     "~~/src/HOL/Library/Infinite_Set"
   198     "~~/src/HOL/Library/Permutation"
   199   theories
   200     Fib
   201     Factorization
   202     Chinese
   203     WilsonRuss
   204     WilsonBij
   205     Quadratic_Reciprocity
   206     Primes
   207     Pocklington
   208   files "document/root.tex"
   209 
   210 session "HOL-Hoare" in Hoare = HOL +
   211   description {*
   212     Verification of imperative programs (verification conditions are generated
   213     automatically from pre/post conditions and loop invariants).
   214   *}
   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_Tests
   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   files
   681     "document/root.tex"
   682 
   683 session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
   684   options [document_graph]
   685   theories [document = false]
   686     "~~/src/HOL/Library/Countable"
   687     "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
   688     "~~/src/HOL/Library/Permutation"
   689   theories
   690     Probability
   691     "ex/Dining_Cryptographers"
   692     "ex/Koepf_Duermuth_Countermeasure"
   693   files "document/root.tex"
   694 
   695 session "HOL-Nominal" (main) in Nominal = HOL +
   696   options [document = false]
   697   theories Nominal
   698 
   699 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
   700   options [timeout = 3600, condition = ISABELLE_POLYML, document = false]
   701   theories Nominal_Examples
   702   theories [quick_and_dirty] VC_Condition
   703 
   704 session "HOL-Cardinals" in Cardinals = HOL +
   705   description {*
   706     Ordinals and Cardinals, Full Theories.
   707   *}
   708   options [document = false]
   709   theories Cardinals
   710   files
   711     "document/intro.tex"
   712     "document/root.tex"
   713     "document/root.bib"
   714 
   715 session "HOL-BNF_Examples" in BNF_Examples = HOL +
   716   description {*
   717     Examples for Bounded Natural Functors.
   718   *}
   719   options [document = false]
   720   theories
   721     Lambda_Term
   722     Process
   723     TreeFsetI
   724     "Derivation_Trees/Gram_Lang"
   725     "Derivation_Trees/Parallel"
   726     Koenig
   727     Stream_Processor
   728   theories [condition = ISABELLE_FULL_TEST]
   729     Misc_Codatatype
   730     Misc_Datatype
   731     Misc_Primcorec
   732     Misc_Primrec
   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-Statespace" in Statespace = HOL +
   744   theories [skip_proofs = false]
   745     StateSpaceEx
   746   files "document/root.tex"
   747 
   748 session "HOL-NSA" in NSA = HOL +
   749   description {*
   750     Nonstandard analysis.
   751   *}
   752   options [document_graph]
   753   theories Hypercomplex
   754   files "document/root.tex"
   755 
   756 session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
   757   options [document = false]
   758   theories NSPrimes
   759 
   760 session "HOL-Mirabelle" in Mirabelle = HOL +
   761   options [document = false]
   762   theories Mirabelle_Test
   763 
   764 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   765   options [document = false, timeout = 60]
   766   theories Ex
   767 
   768 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
   769   options [document = false, quick_and_dirty]
   770   theories
   771     Boogie
   772     SMT_Examples
   773     SMT_Word_Examples
   774   theories [condition = ISABELLE_FULL_TEST]
   775     SMT_Tests
   776   files
   777     "Boogie_Dijkstra.certs"
   778     "Boogie_Max.certs"
   779     "SMT_Examples.certs"
   780     "SMT_Word_Examples.certs"
   781     "VCC_Max.certs"
   782 
   783 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   784   options [document = false]
   785   theories SPARK
   786 
   787 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   788   options [document = false]
   789   theories
   790     "Gcd/Greatest_Common_Divisor"
   791 
   792     "Liseq/Longest_Increasing_Subsequence"
   793 
   794     "RIPEMD-160/F"
   795     "RIPEMD-160/Hash"
   796     "RIPEMD-160/K_L"
   797     "RIPEMD-160/K_R"
   798     "RIPEMD-160/R_L"
   799     "RIPEMD-160/Round"
   800     "RIPEMD-160/R_R"
   801     "RIPEMD-160/S_L"
   802     "RIPEMD-160/S_R"
   803 
   804     "Sqrt/Sqrt"
   805   files
   806     "Gcd/greatest_common_divisor/g_c_d.fdl"
   807     "Gcd/greatest_common_divisor/g_c_d.rls"
   808     "Gcd/greatest_common_divisor/g_c_d.siv"
   809     "Liseq/liseq/liseq_length.fdl"
   810     "Liseq/liseq/liseq_length.rls"
   811     "Liseq/liseq/liseq_length.siv"
   812     "RIPEMD-160/rmd/f.fdl"
   813     "RIPEMD-160/rmd/f.rls"
   814     "RIPEMD-160/rmd/f.siv"
   815     "RIPEMD-160/rmd/hash.fdl"
   816     "RIPEMD-160/rmd/hash.rls"
   817     "RIPEMD-160/rmd/hash.siv"
   818     "RIPEMD-160/rmd/k_l.fdl"
   819     "RIPEMD-160/rmd/k_l.rls"
   820     "RIPEMD-160/rmd/k_l.siv"
   821     "RIPEMD-160/rmd/k_r.fdl"
   822     "RIPEMD-160/rmd/k_r.rls"
   823     "RIPEMD-160/rmd/k_r.siv"
   824     "RIPEMD-160/rmd/r_l.fdl"
   825     "RIPEMD-160/rmd/r_l.rls"
   826     "RIPEMD-160/rmd/r_l.siv"
   827     "RIPEMD-160/rmd/round.fdl"
   828     "RIPEMD-160/rmd/round.rls"
   829     "RIPEMD-160/rmd/round.siv"
   830     "RIPEMD-160/rmd/r_r.fdl"
   831     "RIPEMD-160/rmd/r_r.rls"
   832     "RIPEMD-160/rmd/r_r.siv"
   833     "RIPEMD-160/rmd/s_l.fdl"
   834     "RIPEMD-160/rmd/s_l.rls"
   835     "RIPEMD-160/rmd/s_l.siv"
   836     "RIPEMD-160/rmd/s_r.fdl"
   837     "RIPEMD-160/rmd/s_r.rls"
   838     "RIPEMD-160/rmd/s_r.siv"
   839 
   840 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   841   options [show_question_marks = false]
   842   theories
   843     Example_Verification
   844     VC_Principles
   845     Reference
   846     Complex_Types
   847   files
   848     "complex_types_app/initialize.fdl"
   849     "complex_types_app/initialize.rls"
   850     "complex_types_app/initialize.siv"
   851     "document/complex_types.ads"
   852     "document/complex_types_app.adb"
   853     "document/complex_types_app.ads"
   854     "document/Gcd.adb"
   855     "document/Gcd.ads"
   856     "document/intro.tex"
   857     "document/loop_invariant.adb"
   858     "document/loop_invariant.ads"
   859     "document/root.bib"
   860     "document/root.tex"
   861     "document/Simple_Gcd.adb"
   862     "document/Simple_Gcd.ads"
   863     "loop_invariant/proc1.fdl"
   864     "loop_invariant/proc1.rls"
   865     "loop_invariant/proc1.siv"
   866     "loop_invariant/proc2.fdl"
   867     "loop_invariant/proc2.rls"
   868     "loop_invariant/proc2.siv"
   869     "simple_greatest_common_divisor/g_c_d.fdl"
   870     "simple_greatest_common_divisor/g_c_d.rls"
   871     "simple_greatest_common_divisor/g_c_d.siv"
   872 
   873 session "HOL-Mutabelle" in Mutabelle = HOL +
   874   options [document = false]
   875   theories MutabelleExtra
   876 
   877 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
   878   options [document = false]
   879   theories
   880     Quickcheck_Examples
   881   (* FIXME
   882     Quickcheck_Lattice_Examples
   883     Completeness
   884     Quickcheck_Interfaces
   885     Hotel_Example *)
   886   theories [condition = ISABELLE_GHC]
   887     Quickcheck_Narrowing_Examples
   888 
   889 session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
   890   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
   891     Find_Unused_Assms_Examples
   892     Needham_Schroeder_No_Attacker_Example
   893     Needham_Schroeder_Guided_Attacker_Example
   894     Needham_Schroeder_Unguided_Attacker_Example
   895 
   896 session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
   897   description {*
   898     Author:     Cezary Kaliszyk and Christian Urban
   899   *}
   900   options [document = false]
   901   theories
   902     DList
   903     FSet
   904     Quotient_Int
   905     Quotient_Message
   906     Lift_FSet
   907     Lift_Set
   908     Lift_Fun
   909     Quotient_Rat
   910     Lift_DList
   911     Int_Pow
   912 
   913 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   914   options [document = false]
   915   theories
   916     Examples
   917     Predicate_Compile_Tests
   918     (* FIXME
   919     Predicate_Compile_Quickcheck_Examples  -- should be added again soon (since 21-Oct-2010) *)
   920     Specialisation_Examples
   921     IMP_1
   922     IMP_2
   923     (* FIXME since 21-Jul-2011
   924     Hotel_Example_Small_Generator
   925     IMP_3
   926     IMP_4 *)
   927   theories [condition = "ISABELLE_SWIPL"]
   928     Code_Prolog_Examples
   929     Context_Free_Grammar_Example
   930     Hotel_Example_Prolog
   931     Lambda_Example
   932     List_Examples
   933   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]
   934     Reg_Exp_Example
   935 
   936 session HOLCF (main) in HOLCF = HOL +
   937   description {*
   938     Author:     Franz Regensburger
   939     Author:     Brian Huffman
   940 
   941     HOLCF -- a semantic extension of HOL by the LCF logic.
   942   *}
   943   options [document_graph]
   944   theories [document = false]
   945     "~~/src/HOL/Library/Nat_Bijection"
   946     "~~/src/HOL/Library/Countable"
   947   theories
   948     Plain_HOLCF
   949     Fixrec
   950     HOLCF
   951   files "document/root.tex"
   952 
   953 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   954   theories
   955     Domain_ex
   956     Fixrec_ex
   957     New_Domain
   958   files "document/root.tex"
   959 
   960 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   961   options [document = false]
   962   theories HOLCF_Library
   963 
   964 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   965   description {*
   966     IMP -- A WHILE-language and its Semantics.
   967 
   968     This is the HOLCF-based denotational semantics of a simple WHILE-language.
   969   *}
   970   options [document = false]
   971   theories HoareEx
   972   files "document/root.tex"
   973 
   974 session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
   975   description {*
   976     Miscellaneous examples for HOLCF.
   977   *}
   978   options [document = false]
   979   theories
   980     Dnat
   981     Dagstuhl
   982     Focus_ex
   983     Fix2
   984     Hoare
   985     Concurrency_Monad
   986     Loop
   987     Powerdomain_ex
   988     Domain_Proofs
   989     Letrec
   990     Pattern_Match
   991 
   992 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
   993   description {*
   994     FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
   995 
   996     For introductions to FOCUS, see
   997 
   998     "The Design of Distributed Systems - An Introduction to FOCUS"
   999     http://www4.in.tum.de/publ/html.php?e=2
  1000 
  1001     "Specification and Refinement of a Buffer of Length One"
  1002     http://www4.in.tum.de/publ/html.php?e=15
  1003 
  1004     "Specification and Development of Interactive Systems: Focus on Streams,
  1005     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
  1006   *}
  1007   options [document = false]
  1008   theories
  1009     Fstreams
  1010     FOCUS
  1011     Buffer_adm
  1012 
  1013 session IOA in "HOLCF/IOA" = HOLCF +
  1014   description {*
  1015     Author:     Olaf Mueller
  1016     Copyright   1997 TU München
  1017 
  1018     A formalization of I/O automata in HOLCF.
  1019 
  1020     The distribution contains simulation relations, temporal logic, and an
  1021     abstraction theory. Everything is based upon a domain-theoretic model of
  1022     finite and infinite sequences.
  1023   *}
  1024   options [document = false]
  1025   theories "meta_theory/Abstraction"
  1026 
  1027 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  1028   description {*
  1029     Author:     Olaf Mueller
  1030 
  1031     The Alternating Bit Protocol performed in I/O-Automata.
  1032   *}
  1033   options [document = false]
  1034   theories Correctness
  1035 
  1036 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
  1037   description {*
  1038     Author:     Tobias Nipkow & Konrad Slind
  1039 
  1040     A network transmission protocol, performed in the
  1041     I/O automata formalization by Olaf Mueller.
  1042   *}
  1043   options [document = false]
  1044   theories Correctness
  1045 
  1046 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
  1047   description {*
  1048     Author:     Olaf Mueller
  1049 
  1050     Memory storage case study.
  1051   *}
  1052   options [document = false]
  1053   theories Correctness
  1054 
  1055 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
  1056   description {*
  1057     Author:     Olaf Mueller
  1058   *}
  1059   options [document = false]
  1060   theories
  1061     TrivEx
  1062     TrivEx2
  1063 
  1064 session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
  1065   description {*
  1066     Some rather large datatype examples (from John Harrison).
  1067   *}
  1068   options [document = false]
  1069   theories [condition = ISABELLE_FULL_TEST, timing]
  1070     Brackin
  1071     Instructions
  1072     SML
  1073     Verilog
  1074 
  1075 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
  1076   description {*
  1077     Some benchmark on large record.
  1078   *}
  1079   options [document = false]
  1080   theories [condition = ISABELLE_FULL_TEST, timing]
  1081     Record_Benchmark
  1082