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