src/HOL/ROOT
author haftmann
Thu Apr 24 10:33:17 2014 +0200 (2014-04-24)
changeset 56680 4e2a0d4e7a82
parent 56676 015f9e5e4fae
child 56781 f2eb0f22589f
permissions -rw-r--r--
now covered by AFP 3ddac3e572cf
     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     Gauge_Integration
   564     Dedekind_Real
   565     Quicksort
   566     Birthday_Paradox
   567     List_to_Set_Comprehension_Examples
   568     Seq
   569     Simproc_Tests
   570     Executable_Relation
   571     FinFunPred
   572     Set_Comprehension_Pointfree_Examples
   573     Parallel_Example
   574     IArray_Examples
   575     SVC_Oracle
   576     Simps_Case_Conv_Examples
   577     ML
   578   theories [skip_proofs = false]
   579     Meson_Test
   580   theories [condition = SVC_HOME]
   581     svc_test
   582   theories [condition = ZCHAFF_HOME]
   583     (*requires zChaff (or some other reasonably fast SAT solver)*)
   584     Sudoku
   585 (* FIXME
   586 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
   587     SAT_Examples
   588 *)
   589   files "document/root.bib" "document/root.tex"
   590 
   591 session "HOL-Isar_Examples" in Isar_Examples = HOL +
   592   description {*
   593     Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
   594   *}
   595   theories [document = false]
   596     "~~/src/HOL/Library/Lattice_Syntax"
   597     "../Number_Theory/Primes"
   598   theories
   599     Basic_Logic
   600     Cantor
   601     Drinker
   602     Expr_Compiler
   603     Fibonacci
   604     Group
   605     Group_Context
   606     Group_Notepad
   607     Hoare_Ex
   608     Knaster_Tarski
   609     Mutilated_Checkerboard
   610     Nested_Datatype
   611     Peirce
   612     Puzzle
   613     Summation
   614   files
   615     "document/root.bib"
   616     "document/root.tex"
   617     "document/style.tex"
   618 
   619 session "HOL-SET_Protocol" in SET_Protocol = HOL +
   620   description {*
   621     Verification of the SET Protocol.
   622   *}
   623   options [document_graph]
   624   theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
   625   theories SET_Protocol
   626   files "document/root.tex"
   627 
   628 session "HOL-Matrix_LP" in Matrix_LP = HOL +
   629   description {*
   630     Two-dimensional matrices and linear programming.
   631   *}
   632   options [document_graph]
   633   theories Cplex
   634   files "document/root.tex"
   635 
   636 session "HOL-TLA" in TLA = HOL +
   637   description {*
   638     Lamport's Temporal Logic of Actions.
   639   *}
   640   options [document = false]
   641   theories TLA
   642 
   643 session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
   644   options [document = false]
   645   theories Inc
   646 
   647 session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
   648   options [document = false]
   649   theories DBuffer
   650 
   651 session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
   652   options [document = false]
   653   theories MemoryImplementation
   654 
   655 session "HOL-TPTP" in TPTP = HOL +
   656   description {*
   657     Author:     Jasmin Blanchette, TU Muenchen
   658     Author:     Nik Sultana, University of Cambridge
   659     Copyright   2011
   660 
   661     TPTP-related extensions.
   662   *}
   663   options [document = false]
   664   theories
   665     ATP_Theory_Export
   666     MaSh_Eval
   667     MaSh_Export
   668     TPTP_Interpret
   669     THF_Arith
   670     TPTP_Proof_Reconstruction
   671   theories
   672     ATP_Problem_Import
   673 
   674 session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +
   675   options [document_graph]
   676   theories
   677     Multivariate_Analysis
   678     Determinants
   679     PolyRoots
   680     Complex_Analysis_Basics
   681   files
   682     "document/root.tex"
   683 
   684 session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
   685   options [document_graph]
   686   theories [document = false]
   687     "~~/src/HOL/Library/Countable"
   688     "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
   689     "~~/src/HOL/Library/Permutation"
   690   theories
   691     Probability
   692     "ex/Dining_Cryptographers"
   693     "ex/Koepf_Duermuth_Countermeasure"
   694   files "document/root.tex"
   695 
   696 session "HOL-Nominal" (main) in Nominal = HOL +
   697   options [document = false]
   698   theories Nominal
   699 
   700 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
   701   options [timeout = 3600, condition = ISABELLE_POLYML, document = false]
   702   theories Nominal_Examples
   703   theories [quick_and_dirty] VC_Condition
   704 
   705 session "HOL-Cardinals" in Cardinals = HOL +
   706   description {*
   707     Ordinals and Cardinals, Full Theories.
   708   *}
   709   options [document = false]
   710   theories Cardinals
   711   files
   712     "document/intro.tex"
   713     "document/root.tex"
   714     "document/root.bib"
   715 
   716 session "HOL-BNF_Examples" in BNF_Examples = HOL +
   717   description {*
   718     Examples for Bounded Natural Functors.
   719   *}
   720   options [document = false]
   721   theories
   722     Compat
   723     Lambda_Term
   724     Process
   725     TreeFsetI
   726     "Derivation_Trees/Gram_Lang"
   727     "Derivation_Trees/Parallel"
   728     Koenig
   729     Stream_Processor
   730     Misc_Codatatype
   731     Misc_Datatype
   732     Misc_Primcorec
   733     Misc_Primrec
   734 
   735 session "HOL-Word" (main) in Word = HOL +
   736   options [document_graph]
   737   theories Word
   738   files "document/root.bib" "document/root.tex"
   739 
   740 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   741   options [document = false]
   742   theories WordExamples
   743 
   744 session "HOL-Statespace" in Statespace = HOL +
   745   theories [skip_proofs = false]
   746     StateSpaceEx
   747   files "document/root.tex"
   748 
   749 session "HOL-NSA" in NSA = HOL +
   750   description {*
   751     Nonstandard analysis.
   752   *}
   753   options [document_graph]
   754   theories Hypercomplex
   755   files "document/root.tex"
   756 
   757 session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
   758   options [document = false]
   759   theories NSPrimes
   760 
   761 session "HOL-Mirabelle" in Mirabelle = HOL +
   762   options [document = false]
   763   theories Mirabelle_Test
   764 
   765 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   766   options [document = false, timeout = 60]
   767   theories Ex
   768 
   769 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
   770   options [document = false, quick_and_dirty]
   771   theories
   772     Boogie
   773     SMT_Examples
   774     SMT_Word_Examples
   775   theories [condition = ISABELLE_FULL_TEST]
   776     SMT_Tests
   777   files
   778     "Boogie_Dijkstra.certs"
   779     "Boogie_Max.certs"
   780     "SMT_Examples.certs"
   781     "SMT_Examples.certs2"
   782     "SMT_Word_Examples.certs2"
   783     "VCC_Max.certs"
   784 
   785 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   786   options [document = false]
   787   theories SPARK
   788 
   789 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   790   options [document = false]
   791   theories
   792     "Gcd/Greatest_Common_Divisor"
   793 
   794     "Liseq/Longest_Increasing_Subsequence"
   795 
   796     "RIPEMD-160/F"
   797     "RIPEMD-160/Hash"
   798     "RIPEMD-160/K_L"
   799     "RIPEMD-160/K_R"
   800     "RIPEMD-160/R_L"
   801     "RIPEMD-160/Round"
   802     "RIPEMD-160/R_R"
   803     "RIPEMD-160/S_L"
   804     "RIPEMD-160/S_R"
   805 
   806     "Sqrt/Sqrt"
   807   files
   808     "Gcd/greatest_common_divisor/g_c_d.fdl"
   809     "Gcd/greatest_common_divisor/g_c_d.rls"
   810     "Gcd/greatest_common_divisor/g_c_d.siv"
   811     "Liseq/liseq/liseq_length.fdl"
   812     "Liseq/liseq/liseq_length.rls"
   813     "Liseq/liseq/liseq_length.siv"
   814     "RIPEMD-160/rmd/f.fdl"
   815     "RIPEMD-160/rmd/f.rls"
   816     "RIPEMD-160/rmd/f.siv"
   817     "RIPEMD-160/rmd/hash.fdl"
   818     "RIPEMD-160/rmd/hash.rls"
   819     "RIPEMD-160/rmd/hash.siv"
   820     "RIPEMD-160/rmd/k_l.fdl"
   821     "RIPEMD-160/rmd/k_l.rls"
   822     "RIPEMD-160/rmd/k_l.siv"
   823     "RIPEMD-160/rmd/k_r.fdl"
   824     "RIPEMD-160/rmd/k_r.rls"
   825     "RIPEMD-160/rmd/k_r.siv"
   826     "RIPEMD-160/rmd/r_l.fdl"
   827     "RIPEMD-160/rmd/r_l.rls"
   828     "RIPEMD-160/rmd/r_l.siv"
   829     "RIPEMD-160/rmd/round.fdl"
   830     "RIPEMD-160/rmd/round.rls"
   831     "RIPEMD-160/rmd/round.siv"
   832     "RIPEMD-160/rmd/r_r.fdl"
   833     "RIPEMD-160/rmd/r_r.rls"
   834     "RIPEMD-160/rmd/r_r.siv"
   835     "RIPEMD-160/rmd/s_l.fdl"
   836     "RIPEMD-160/rmd/s_l.rls"
   837     "RIPEMD-160/rmd/s_l.siv"
   838     "RIPEMD-160/rmd/s_r.fdl"
   839     "RIPEMD-160/rmd/s_r.rls"
   840     "RIPEMD-160/rmd/s_r.siv"
   841 
   842 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   843   options [show_question_marks = false]
   844   theories
   845     Example_Verification
   846     VC_Principles
   847     Reference
   848     Complex_Types
   849   files
   850     "complex_types_app/initialize.fdl"
   851     "complex_types_app/initialize.rls"
   852     "complex_types_app/initialize.siv"
   853     "document/complex_types.ads"
   854     "document/complex_types_app.adb"
   855     "document/complex_types_app.ads"
   856     "document/Gcd.adb"
   857     "document/Gcd.ads"
   858     "document/intro.tex"
   859     "document/loop_invariant.adb"
   860     "document/loop_invariant.ads"
   861     "document/root.bib"
   862     "document/root.tex"
   863     "document/Simple_Gcd.adb"
   864     "document/Simple_Gcd.ads"
   865     "loop_invariant/proc1.fdl"
   866     "loop_invariant/proc1.rls"
   867     "loop_invariant/proc1.siv"
   868     "loop_invariant/proc2.fdl"
   869     "loop_invariant/proc2.rls"
   870     "loop_invariant/proc2.siv"
   871     "simple_greatest_common_divisor/g_c_d.fdl"
   872     "simple_greatest_common_divisor/g_c_d.rls"
   873     "simple_greatest_common_divisor/g_c_d.siv"
   874 
   875 session "HOL-Mutabelle" in Mutabelle = HOL +
   876   options [document = false]
   877   theories MutabelleExtra
   878 
   879 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
   880   options [document = false]
   881   theories
   882     Quickcheck_Examples
   883   (* FIXME
   884     Quickcheck_Lattice_Examples
   885     Completeness
   886     Quickcheck_Interfaces
   887     Hotel_Example *)
   888   theories [condition = ISABELLE_GHC]
   889     Quickcheck_Narrowing_Examples
   890 
   891 session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
   892   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
   893     Find_Unused_Assms_Examples
   894     Needham_Schroeder_No_Attacker_Example
   895     Needham_Schroeder_Guided_Attacker_Example
   896     Needham_Schroeder_Unguided_Attacker_Example
   897 
   898 session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
   899   description {*
   900     Author:     Cezary Kaliszyk and Christian Urban
   901   *}
   902   options [document = false]
   903   theories
   904     DList
   905     FSet
   906     Quotient_Int
   907     Quotient_Message
   908     Lift_FSet
   909     Lift_Set
   910     Lift_Fun
   911     Quotient_Rat
   912     Lift_DList
   913     Int_Pow
   914 
   915 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   916   options [document = false]
   917   theories
   918     Examples
   919     Predicate_Compile_Tests
   920     (* FIXME
   921     Predicate_Compile_Quickcheck_Examples  -- should be added again soon (since 21-Oct-2010) *)
   922     Specialisation_Examples
   923     IMP_1
   924     IMP_2
   925     (* FIXME since 21-Jul-2011
   926     Hotel_Example_Small_Generator
   927     IMP_3
   928     IMP_4 *)
   929   theories [condition = "ISABELLE_SWIPL"]
   930     Code_Prolog_Examples
   931     Context_Free_Grammar_Example
   932     Hotel_Example_Prolog
   933     Lambda_Example
   934     List_Examples
   935   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]
   936     Reg_Exp_Example
   937 
   938 session HOLCF (main) in HOLCF = HOL +
   939   description {*
   940     Author:     Franz Regensburger
   941     Author:     Brian Huffman
   942 
   943     HOLCF -- a semantic extension of HOL by the LCF logic.
   944   *}
   945   options [document_graph]
   946   theories [document = false]
   947     "~~/src/HOL/Library/Nat_Bijection"
   948     "~~/src/HOL/Library/Countable"
   949   theories
   950     Plain_HOLCF
   951     Fixrec
   952     HOLCF
   953   files "document/root.tex"
   954 
   955 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   956   theories
   957     Domain_ex
   958     Fixrec_ex
   959     New_Domain
   960   files "document/root.tex"
   961 
   962 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   963   options [document = false]
   964   theories HOLCF_Library
   965 
   966 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   967   description {*
   968     IMP -- A WHILE-language and its Semantics.
   969 
   970     This is the HOLCF-based denotational semantics of a simple WHILE-language.
   971   *}
   972   options [document = false]
   973   theories HoareEx
   974   files "document/root.tex"
   975 
   976 session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
   977   description {*
   978     Miscellaneous examples for HOLCF.
   979   *}
   980   options [document = false]
   981   theories
   982     Dnat
   983     Dagstuhl
   984     Focus_ex
   985     Fix2
   986     Hoare
   987     Concurrency_Monad
   988     Loop
   989     Powerdomain_ex
   990     Domain_Proofs
   991     Letrec
   992     Pattern_Match
   993 
   994 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
   995   description {*
   996     FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
   997 
   998     For introductions to FOCUS, see
   999 
  1000     "The Design of Distributed Systems - An Introduction to FOCUS"
  1001     http://www4.in.tum.de/publ/html.php?e=2
  1002 
  1003     "Specification and Refinement of a Buffer of Length One"
  1004     http://www4.in.tum.de/publ/html.php?e=15
  1005 
  1006     "Specification and Development of Interactive Systems: Focus on Streams,
  1007     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
  1008   *}
  1009   options [document = false]
  1010   theories
  1011     Fstreams
  1012     FOCUS
  1013     Buffer_adm
  1014 
  1015 session IOA in "HOLCF/IOA" = HOLCF +
  1016   description {*
  1017     Author:     Olaf Mueller
  1018     Copyright   1997 TU München
  1019 
  1020     A formalization of I/O automata in HOLCF.
  1021 
  1022     The distribution contains simulation relations, temporal logic, and an
  1023     abstraction theory. Everything is based upon a domain-theoretic model of
  1024     finite and infinite sequences.
  1025   *}
  1026   options [document = false]
  1027   theories "meta_theory/Abstraction"
  1028 
  1029 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  1030   description {*
  1031     Author:     Olaf Mueller
  1032 
  1033     The Alternating Bit Protocol performed in I/O-Automata.
  1034   *}
  1035   options [document = false]
  1036   theories Correctness
  1037 
  1038 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
  1039   description {*
  1040     Author:     Tobias Nipkow & Konrad Slind
  1041 
  1042     A network transmission protocol, performed in the
  1043     I/O automata formalization by Olaf Mueller.
  1044   *}
  1045   options [document = false]
  1046   theories Correctness
  1047 
  1048 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
  1049   description {*
  1050     Author:     Olaf Mueller
  1051 
  1052     Memory storage case study.
  1053   *}
  1054   options [document = false]
  1055   theories Correctness
  1056 
  1057 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
  1058   description {*
  1059     Author:     Olaf Mueller
  1060   *}
  1061   options [document = false]
  1062   theories
  1063     TrivEx
  1064     TrivEx2
  1065 
  1066 session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
  1067   description {*
  1068     Some rather large datatype examples (from John Harrison).
  1069   *}
  1070   options [document = false]
  1071   theories [condition = ISABELLE_FULL_TEST, timing]
  1072     Brackin
  1073     Instructions
  1074     SML
  1075     Verilog
  1076 
  1077 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
  1078   description {*
  1079     Some benchmark on large record.
  1080   *}
  1081   options [document = false]
  1082   theories [condition = ISABELLE_FULL_TEST, timing]
  1083     Record_Benchmark
  1084