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