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