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