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