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