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