src/HOL/ROOT
author wenzelm
Sun Jan 25 22:11:06 2015 +0100 (2015-01-25)
changeset 59446 4427f04fca57
parent 59190 3a594fd13ca4
child 59503 9937bc07202b
permissions -rw-r--r--
discontinued obsolete option "document_graph";
     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/Number_Theory/Binomial"
   289     "~~/src/HOL/Library/Permutation"
   290   theories
   291     (*** New development, based on explicit structures ***)
   292     (* Groups *)
   293     FiniteProduct        (* Product operator for commutative groups *)
   294     Sylow                (* Sylow's theorem *)
   295     Bij                  (* Automorphism Groups *)
   296 
   297     (* Rings *)
   298     Divisibility         (* Rings *)
   299     IntRing              (* Ideals and residue classes *)
   300     UnivPoly             (* Polynomials *)
   301   document_files "root.bib" "root.tex"
   302 
   303 session "HOL-Auth" in Auth = HOL +
   304   description {*
   305     A new approach to verifying authentication protocols.
   306   *}
   307   theories
   308     Auth_Shared
   309     Auth_Public
   310     "Smartcard/Auth_Smartcard"
   311     "Guard/Auth_Guard_Shared"
   312     "Guard/Auth_Guard_Public"
   313   document_files "root.tex"
   314 
   315 session "HOL-UNITY" in UNITY = "HOL-Auth" +
   316   description {*
   317     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   318     Copyright   1998  University of Cambridge
   319 
   320     Verifying security protocols using Chandy and Misra's UNITY formalism.
   321   *}
   322   theories
   323     (*Basic meta-theory*)
   324     "UNITY_Main"
   325 
   326     (*Simple examples: no composition*)
   327     "Simple/Deadlock"
   328     "Simple/Common"
   329     "Simple/Network"
   330     "Simple/Token"
   331     "Simple/Channel"
   332     "Simple/Lift"
   333     "Simple/Mutex"
   334     "Simple/Reach"
   335     "Simple/Reachability"
   336 
   337     (*Verifying security protocols using UNITY*)
   338     "Simple/NSP_Bad"
   339 
   340     (*Example of composition*)
   341     "Comp/Handshake"
   342 
   343     (*Universal properties examples*)
   344     "Comp/Counter"
   345     "Comp/Counterc"
   346     "Comp/Priority"
   347 
   348     "Comp/TimerArray"
   349     "Comp/Progress"
   350 
   351     "Comp/Alloc"
   352     "Comp/AllocImpl"
   353     "Comp/Client"
   354 
   355     (*obsolete*)
   356     "ELT"
   357   document_files "root.tex"
   358 
   359 session "HOL-Unix" in Unix = HOL +
   360   options [print_mode = "no_brackets,no_type_brackets"]
   361   theories Unix
   362   document_files "root.bib" "root.tex"
   363 
   364 session "HOL-ZF" in ZF = HOL +
   365   theories MainZF Games
   366   document_files "root.tex"
   367 
   368 session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
   369   options [print_mode = "iff,no_brackets"]
   370   theories [document = false]
   371     "~~/src/HOL/Library/Countable"
   372     "~~/src/HOL/Library/Monad_Syntax"
   373     "~~/src/HOL/Library/LaTeXsugar"
   374   theories Imperative_HOL_ex
   375   document_files "root.bib" "root.tex"
   376 
   377 session "HOL-Decision_Procs" in Decision_Procs = HOL +
   378   description {*
   379     Various decision procedures, typically involving reflection.
   380   *}
   381   options [condition = ML_SYSTEM_POLYML, document = false]
   382   theories Decision_Procs
   383 
   384 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
   385   options [document = false, parallel_proofs = 0]
   386   theories
   387     Hilbert_Classical
   388     XML_Data
   389 
   390 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
   391   description {*
   392     Examples for program extraction in Higher-Order Logic.
   393   *}
   394   options [condition = ML_SYSTEM_POLYML, parallel_proofs = 0, quick_and_dirty = false]
   395   theories [document = false]
   396     "~~/src/HOL/Library/Code_Target_Numeral"
   397     "~~/src/HOL/Library/Monad_Syntax"
   398     "~~/src/HOL/Number_Theory/Primes"
   399     "~~/src/HOL/Number_Theory/UniqueFactorization"
   400     "~~/src/HOL/Library/State_Monad"
   401   theories
   402     Greatest_Common_Divisor
   403     Warshall
   404     Higman_Extraction
   405     Pigeonhole
   406     Euclid
   407   document_files "root.bib" "root.tex"
   408 
   409 session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +
   410   description {*
   411     Lambda Calculus in de Bruijn's Notation.
   412 
   413     This session defines lambda-calculus terms with de Bruijn indixes and
   414     proves confluence of beta, eta and beta+eta.
   415 
   416     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
   417     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
   418   *}
   419   options [print_mode = "no_brackets", parallel_proofs = 0, quick_and_dirty = false]
   420   theories [document = false]
   421     "~~/src/HOL/Library/Code_Target_Int"
   422   theories
   423     Eta
   424     StrongNorm
   425     Standardization
   426     WeakNorm
   427   document_files "root.bib" "root.tex"
   428 
   429 session "HOL-Prolog" in Prolog = HOL +
   430   description {*
   431     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
   432 
   433     A bare-bones implementation of Lambda-Prolog.
   434 
   435     This is a simple exploratory implementation of Lambda-Prolog in HOL,
   436     including some minimal examples (in Test.thy) and a more typical example of
   437     a little functional language and its type system.
   438   *}
   439   options [document = false]
   440   theories Test Type
   441 
   442 session "HOL-MicroJava" in MicroJava = HOL +
   443   description {*
   444     Formalization of a fragment of Java, together with a corresponding virtual
   445     machine and a specification of its bytecode verifier and a lightweight
   446     bytecode verifier, including proofs of type-safety.
   447   *}
   448   theories [document = false]
   449     "~~/src/HOL/Library/While_Combinator"
   450   theories
   451     MicroJava
   452   document_files
   453     "introduction.tex"
   454     "root.bib"
   455     "root.tex"
   456 
   457 session "HOL-NanoJava" in NanoJava = HOL +
   458   description {*
   459     Hoare Logic for a tiny fragment of Java.
   460   *}
   461   theories Example
   462   document_files "root.bib" "root.tex"
   463 
   464 session "HOL-Bali" in Bali = HOL +
   465   theories
   466     AxExample
   467     AxSound
   468     AxCompl
   469     Trans
   470   document_files "root.tex"
   471 
   472 session "HOL-IOA" in IOA = HOL +
   473   description {*
   474     Author:     Tobias Nipkow and Konrad Slind and Olaf Müller
   475     Copyright   1994--1996  TU Muenchen
   476 
   477     The meta-theory of I/O-Automata in HOL. This formalization has been
   478     significantly changed and extended, see HOLCF/IOA. There are also the
   479     proofs of two communication protocols which formerly have been here.
   480 
   481     @inproceedings{Nipkow-Slind-IOA,
   482     author={Tobias Nipkow and Konrad Slind},
   483     title={{I/O} Automata in {Isabelle/HOL}},
   484     booktitle={Proc.\ TYPES Workshop 1994},
   485     publisher=Springer,
   486     series=LNCS,
   487     note={To appear}}
   488     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
   489 
   490     and
   491 
   492     @inproceedings{Mueller-Nipkow,
   493     author={Olaf M\"uller and Tobias Nipkow},
   494     title={Combining Model Checking and Deduction for {I/O}-Automata},
   495     booktitle={Proc.\ TACAS Workshop},
   496     organization={Aarhus University, BRICS report},
   497     year=1995}
   498     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
   499   *}
   500   options [document = false]
   501   theories Solve
   502 
   503 session "HOL-Lattice" in Lattice = HOL +
   504   description {*
   505     Author:     Markus Wenzel, TU Muenchen
   506 
   507     Basic theory of lattices and orders.
   508   *}
   509   theories CompleteLattice
   510   document_files "root.tex"
   511 
   512 session "HOL-ex" in ex = HOL +
   513   description {*
   514     Miscellaneous examples for Higher-Order Logic.
   515   *}
   516   options [condition = ML_SYSTEM_POLYML]
   517   theories [document = false]
   518     "~~/src/HOL/Library/State_Monad"
   519     Code_Binary_Nat_examples
   520     "~~/src/HOL/Library/FuncSet"
   521     Eval_Examples
   522     Normalization_by_Evaluation
   523     Hebrew
   524     Chinese
   525     Serbian
   526     "~~/src/HOL/Library/FinFun_Syntax"
   527     "~~/src/HOL/Library/Refute"
   528     "~~/src/HOL/Library/Transitive_Closure_Table"
   529     Cartouche_Examples
   530   theories
   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     BT
   557     Tree23
   558     Bubblesort
   559     MergeSort
   560     Lagrange
   561     Groebner_Examples
   562     MT
   563     Unification
   564     Primrec
   565     Tarski
   566     Classical
   567     Set_Theory
   568     Termination
   569     Coherent
   570     PresburgerEx
   571     Reflection_Examples
   572     Sqrt
   573     Sqrt_Script
   574     Transfer_Ex
   575     Transfer_Int_Nat
   576     Transitive_Closure_Table_Ex
   577     HarmonicSeries
   578     Refute_Examples
   579     Execute_Choice
   580     Gauge_Integration
   581     Dedekind_Real
   582     Quicksort
   583     Birthday_Paradox
   584     List_to_Set_Comprehension_Examples
   585     Seq
   586     Simproc_Tests
   587     Executable_Relation
   588     FinFunPred
   589     Set_Comprehension_Pointfree_Examples
   590     Parallel_Example
   591     IArray_Examples
   592     SVC_Oracle
   593     Simps_Case_Conv_Examples
   594     ML
   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   document_files
   693     "root.tex"
   694 
   695 session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
   696   theories [document = false]
   697     "~~/src/HOL/Library/Countable"
   698     "~~/src/HOL/Library/Permutation"
   699     "~~/src/HOL/Library/Order_Continuity"
   700     "~~/src/HOL/Library/Diagonal_Subsequence"
   701   theories
   702     Probability
   703     "ex/Dining_Cryptographers"
   704     "ex/Koepf_Duermuth_Countermeasure"
   705     "ex/Measure_Not_CCC"
   706   document_files "root.tex"
   707 
   708 session "HOL-Nominal" (main) in Nominal = HOL +
   709   options [document = false]
   710   theories Nominal
   711 
   712 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
   713   options [condition = ML_SYSTEM_POLYML, document = false]
   714   theories
   715     Class3
   716     CK_Machine
   717     Compile
   718     Contexts
   719     Crary
   720     CR_Takahashi
   721     CR
   722     Fsub
   723     Height
   724     Lambda_mu
   725     Lam_Funs
   726     LocalWeakening
   727     Pattern
   728     SN
   729     SOS
   730     Standardization
   731     Support
   732     Type_Preservation
   733     Weakening
   734     W
   735   theories [quick_and_dirty]
   736     VC_Condition
   737 
   738 session "HOL-Cardinals" in Cardinals = HOL +
   739   description {*
   740     Ordinals and Cardinals, Full Theories.
   741   *}
   742   options [document = false]
   743   theories Cardinals
   744   document_files
   745     "intro.tex"
   746     "root.tex"
   747     "root.bib"
   748 
   749 session "HOL-Datatype_Examples" in Datatype_Examples = HOL +
   750   description {*
   751     (Co)datatype Examples, including large ones from John Harrison.
   752   *}
   753   options [document = false]
   754   theories
   755     "~~/src/HOL/Library/Old_Datatype"
   756     Compat
   757     Lambda_Term
   758     Process
   759     TreeFsetI
   760     "Derivation_Trees/Gram_Lang"
   761     "Derivation_Trees/Parallel"
   762     Koenig
   763     Stream_Processor
   764     Misc_Codatatype
   765     Misc_Datatype
   766     Misc_Primcorec
   767     Misc_Primrec
   768   theories [condition = ISABELLE_FULL_TEST]
   769     Brackin
   770     IsaFoR
   771     Misc_N2M
   772 
   773 session "HOL-Word" (main) in Word = HOL +
   774   theories Word
   775   document_files "root.bib" "root.tex"
   776 
   777 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   778   options [document = false]
   779   theories WordExamples
   780 
   781 session "HOL-Statespace" in Statespace = HOL +
   782   theories [skip_proofs = false]
   783     StateSpaceEx
   784   document_files "root.tex"
   785 
   786 session "HOL-NSA" in NSA = HOL +
   787   description {*
   788     Nonstandard analysis.
   789   *}
   790   theories Hypercomplex
   791   document_files "root.tex"
   792 
   793 session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
   794   options [document = false]
   795   theories NSPrimes
   796 
   797 session "HOL-Mirabelle" in Mirabelle = HOL +
   798   options [document = false]
   799   theories Mirabelle_Test
   800 
   801 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   802   options [document = false, timeout = 60]
   803   theories Ex
   804 
   805 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
   806   options [document = false, quick_and_dirty]
   807   theories
   808     Boogie
   809     SMT_Examples
   810     SMT_Word_Examples
   811   theories [condition = ISABELLE_FULL_TEST]
   812     SMT_Tests
   813   files
   814     "Boogie_Dijkstra.certs"
   815     "Boogie_Max.certs"
   816     "SMT_Examples.certs"
   817     "SMT_Word_Examples.certs"
   818     "VCC_Max.certs"
   819 
   820 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   821   options [document = false]
   822   theories SPARK
   823 
   824 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   825   options [document = false]
   826   theories
   827     "Gcd/Greatest_Common_Divisor"
   828 
   829     "Liseq/Longest_Increasing_Subsequence"
   830 
   831     "RIPEMD-160/F"
   832     "RIPEMD-160/Hash"
   833     "RIPEMD-160/K_L"
   834     "RIPEMD-160/K_R"
   835     "RIPEMD-160/R_L"
   836     "RIPEMD-160/Round"
   837     "RIPEMD-160/R_R"
   838     "RIPEMD-160/S_L"
   839     "RIPEMD-160/S_R"
   840 
   841     "Sqrt/Sqrt"
   842   files
   843     "Gcd/greatest_common_divisor/g_c_d.fdl"
   844     "Gcd/greatest_common_divisor/g_c_d.rls"
   845     "Gcd/greatest_common_divisor/g_c_d.siv"
   846     "Liseq/liseq/liseq_length.fdl"
   847     "Liseq/liseq/liseq_length.rls"
   848     "Liseq/liseq/liseq_length.siv"
   849     "RIPEMD-160/rmd/f.fdl"
   850     "RIPEMD-160/rmd/f.rls"
   851     "RIPEMD-160/rmd/f.siv"
   852     "RIPEMD-160/rmd/hash.fdl"
   853     "RIPEMD-160/rmd/hash.rls"
   854     "RIPEMD-160/rmd/hash.siv"
   855     "RIPEMD-160/rmd/k_l.fdl"
   856     "RIPEMD-160/rmd/k_l.rls"
   857     "RIPEMD-160/rmd/k_l.siv"
   858     "RIPEMD-160/rmd/k_r.fdl"
   859     "RIPEMD-160/rmd/k_r.rls"
   860     "RIPEMD-160/rmd/k_r.siv"
   861     "RIPEMD-160/rmd/r_l.fdl"
   862     "RIPEMD-160/rmd/r_l.rls"
   863     "RIPEMD-160/rmd/r_l.siv"
   864     "RIPEMD-160/rmd/round.fdl"
   865     "RIPEMD-160/rmd/round.rls"
   866     "RIPEMD-160/rmd/round.siv"
   867     "RIPEMD-160/rmd/r_r.fdl"
   868     "RIPEMD-160/rmd/r_r.rls"
   869     "RIPEMD-160/rmd/r_r.siv"
   870     "RIPEMD-160/rmd/s_l.fdl"
   871     "RIPEMD-160/rmd/s_l.rls"
   872     "RIPEMD-160/rmd/s_l.siv"
   873     "RIPEMD-160/rmd/s_r.fdl"
   874     "RIPEMD-160/rmd/s_r.rls"
   875     "RIPEMD-160/rmd/s_r.siv"
   876 
   877 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   878   options [show_question_marks = false]
   879   theories
   880     Example_Verification
   881     VC_Principles
   882     Reference
   883     Complex_Types
   884   files
   885     "complex_types_app/initialize.fdl"
   886     "complex_types_app/initialize.rls"
   887     "complex_types_app/initialize.siv"
   888     "loop_invariant/proc1.fdl"
   889     "loop_invariant/proc1.rls"
   890     "loop_invariant/proc1.siv"
   891     "loop_invariant/proc2.fdl"
   892     "loop_invariant/proc2.rls"
   893     "loop_invariant/proc2.siv"
   894     "simple_greatest_common_divisor/g_c_d.fdl"
   895     "simple_greatest_common_divisor/g_c_d.rls"
   896     "simple_greatest_common_divisor/g_c_d.siv"
   897   document_files
   898     "complex_types.ads"
   899     "complex_types_app.adb"
   900     "complex_types_app.ads"
   901     "Gcd.adb"
   902     "Gcd.ads"
   903     "intro.tex"
   904     "loop_invariant.adb"
   905     "loop_invariant.ads"
   906     "root.bib"
   907     "root.tex"
   908     "Simple_Gcd.adb"
   909     "Simple_Gcd.ads"
   910 
   911 session "HOL-Mutabelle" in Mutabelle = HOL +
   912   options [document = false]
   913   theories MutabelleExtra
   914 
   915 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
   916   options [document = false]
   917   theories
   918     Quickcheck_Examples
   919     Quickcheck_Lattice_Examples
   920     Completeness
   921     Quickcheck_Interfaces
   922   theories [condition = ISABELLE_GHC]
   923     Hotel_Example
   924     Quickcheck_Narrowing_Examples
   925 
   926 session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
   927   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
   928     Find_Unused_Assms_Examples
   929     Needham_Schroeder_No_Attacker_Example
   930     Needham_Schroeder_Guided_Attacker_Example
   931     Needham_Schroeder_Unguided_Attacker_Example
   932 
   933 session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
   934   description {*
   935     Author:     Cezary Kaliszyk and Christian Urban
   936   *}
   937   options [document = false]
   938   theories
   939     DList
   940     FSet
   941     Quotient_Int
   942     Quotient_Message
   943     Lift_FSet
   944     Lift_Set
   945     Lift_Fun
   946     Quotient_Rat
   947     Lift_DList
   948     Int_Pow
   949 
   950 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   951   options [document = false]
   952   theories
   953     Examples
   954     Predicate_Compile_Tests
   955     (* FIXME
   956     Predicate_Compile_Quickcheck_Examples  -- should be added again soon (since 21-Oct-2010) *)
   957     Specialisation_Examples
   958     IMP_1
   959     IMP_2
   960     (* FIXME since 21-Jul-2011
   961     Hotel_Example_Small_Generator
   962     IMP_3
   963     IMP_4 *)
   964   theories [condition = "ISABELLE_SWIPL"]
   965     Code_Prolog_Examples
   966     Context_Free_Grammar_Example
   967     Hotel_Example_Prolog
   968     Lambda_Example
   969     List_Examples
   970   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]
   971     Reg_Exp_Example
   972 
   973 session HOLCF (main) in HOLCF = HOL +
   974   description {*
   975     Author:     Franz Regensburger
   976     Author:     Brian Huffman
   977 
   978     HOLCF -- a semantic extension of HOL by the LCF logic.
   979   *}
   980   theories [document = false]
   981     "~~/src/HOL/Library/Nat_Bijection"
   982     "~~/src/HOL/Library/Countable"
   983   theories
   984     Plain_HOLCF
   985     Fixrec
   986     HOLCF
   987   document_files "root.tex"
   988 
   989 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   990   theories
   991     Domain_ex
   992     Fixrec_ex
   993     New_Domain
   994   document_files "root.tex"
   995 
   996 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   997   options [document = false]
   998   theories HOLCF_Library
   999 
  1000 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
  1001   description {*
  1002     IMP -- A WHILE-language and its Semantics.
  1003 
  1004     This is the HOLCF-based denotational semantics of a simple WHILE-language.
  1005   *}
  1006   options [document = false]
  1007   theories HoareEx
  1008   document_files "root.tex"
  1009 
  1010 session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
  1011   description {*
  1012     Miscellaneous examples for HOLCF.
  1013   *}
  1014   options [document = false]
  1015   theories
  1016     Dnat
  1017     Dagstuhl
  1018     Focus_ex
  1019     Fix2
  1020     Hoare
  1021     Concurrency_Monad
  1022     Loop
  1023     Powerdomain_ex
  1024     Domain_Proofs
  1025     Letrec
  1026     Pattern_Match
  1027 
  1028 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
  1029   description {*
  1030     FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
  1031 
  1032     For introductions to FOCUS, see
  1033 
  1034     "The Design of Distributed Systems - An Introduction to FOCUS"
  1035     http://www4.in.tum.de/publ/html.php?e=2
  1036 
  1037     "Specification and Refinement of a Buffer of Length One"
  1038     http://www4.in.tum.de/publ/html.php?e=15
  1039 
  1040     "Specification and Development of Interactive Systems: Focus on Streams,
  1041     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
  1042   *}
  1043   options [document = false]
  1044   theories
  1045     Fstreams
  1046     FOCUS
  1047     Buffer_adm
  1048 
  1049 session IOA in "HOLCF/IOA" = HOLCF +
  1050   description {*
  1051     Author:     Olaf Mueller
  1052     Copyright   1997 TU München
  1053 
  1054     A formalization of I/O automata in HOLCF.
  1055 
  1056     The distribution contains simulation relations, temporal logic, and an
  1057     abstraction theory. Everything is based upon a domain-theoretic model of
  1058     finite and infinite sequences.
  1059   *}
  1060   options [document = false]
  1061   theories "meta_theory/Abstraction"
  1062 
  1063 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  1064   description {*
  1065     Author:     Olaf Mueller
  1066 
  1067     The Alternating Bit Protocol performed in I/O-Automata.
  1068   *}
  1069   options [document = false]
  1070   theories Correctness
  1071 
  1072 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
  1073   description {*
  1074     Author:     Tobias Nipkow & Konrad Slind
  1075 
  1076     A network transmission protocol, performed in the
  1077     I/O automata formalization by Olaf Mueller.
  1078   *}
  1079   options [document = false]
  1080   theories Correctness
  1081 
  1082 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
  1083   description {*
  1084     Author:     Olaf Mueller
  1085 
  1086     Memory storage case study.
  1087   *}
  1088   options [document = false]
  1089   theories Correctness
  1090 
  1091 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
  1092   description {*
  1093     Author:     Olaf Mueller
  1094   *}
  1095   options [document = false]
  1096   theories
  1097     TrivEx
  1098     TrivEx2
  1099 
  1100 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
  1101   description {*
  1102     Some benchmark on large record.
  1103   *}
  1104   options [document = false]
  1105   theories [condition = ISABELLE_FULL_TEST]
  1106     Record_Benchmark
  1107