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