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