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