src/HOL/ROOT
author haftmann
Mon Oct 03 14:37:06 2016 +0200 (2016-10-03)
changeset 64015 c9f3a94cb825
parent 63980 f8e556c8ad6f
child 64282 261d42f0bfac
permissions -rw-r--r--
proof of concept for algebraically founded word types
     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     Word_Type
   631   theories [skip_proofs = false]
   632     Meson_Test
   633   document_files "root.bib" "root.tex"
   634 
   635 session "HOL-Isar_Examples" in Isar_Examples = HOL +
   636   description {*
   637     Miscellaneous Isabelle/Isar examples.
   638   *}
   639   options [quick_and_dirty]
   640   theories [document = false]
   641     "~~/src/HOL/Library/Lattice_Syntax"
   642     "../Number_Theory/Primes"
   643   theories
   644     Knaster_Tarski
   645     Peirce
   646     Drinker
   647     Cantor
   648     Structured_Statements
   649     Basic_Logic
   650     Expr_Compiler
   651     Fibonacci
   652     Group
   653     Group_Context
   654     Group_Notepad
   655     Hoare_Ex
   656     Mutilated_Checkerboard
   657     Puzzle
   658     Summation
   659     First_Order_Logic
   660     Higher_Order_Logic
   661   document_files
   662     "root.bib"
   663     "root.tex"
   664 
   665 session "HOL-Eisbach" in Eisbach = HOL +
   666   description {*
   667     The Eisbach proof method language and "match" method.
   668   *}
   669   theories
   670     Eisbach
   671     Tests
   672     Examples
   673     Examples_FOL
   674 
   675 session "HOL-SET_Protocol" (timing) in SET_Protocol = HOL +
   676   description {*
   677     Verification of the SET Protocol.
   678   *}
   679   theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
   680   theories SET_Protocol
   681   document_files "root.tex"
   682 
   683 session "HOL-Matrix_LP" in Matrix_LP = HOL +
   684   description {*
   685     Two-dimensional matrices and linear programming.
   686   *}
   687   theories Cplex
   688   document_files "root.tex"
   689 
   690 session "HOL-TLA" in TLA = HOL +
   691   description {*
   692     Lamport's Temporal Logic of Actions.
   693   *}
   694   options [document = false]
   695   theories TLA
   696 
   697 session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
   698   options [document = false]
   699   theories Inc
   700 
   701 session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
   702   options [document = false]
   703   theories DBuffer
   704 
   705 session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
   706   options [document = false]
   707   theories MemoryImplementation
   708 
   709 session "HOL-TPTP" in TPTP = HOL +
   710   description {*
   711     Author:     Jasmin Blanchette, TU Muenchen
   712     Author:     Nik Sultana, University of Cambridge
   713     Copyright   2011
   714 
   715     TPTP-related extensions.
   716   *}
   717   options [document = false]
   718   theories
   719     ATP_Theory_Export
   720     MaSh_Eval
   721     TPTP_Interpret
   722     THF_Arith
   723     TPTP_Proof_Reconstruction
   724   theories
   725     ATP_Problem_Import
   726 
   727 session "HOL-Analysis" (main timing) in Analysis = HOL +
   728   theories
   729     Analysis
   730   document_files
   731     "root.tex"
   732 
   733 session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" +
   734   theories
   735     Approximations
   736 
   737 session "HOL-Probability" (timing) in "Probability" = "HOL-Analysis" +
   738   theories [document = false]
   739     "~~/src/HOL/Library/Countable"
   740     "~~/src/HOL/Library/Permutation"
   741     "~~/src/HOL/Library/Order_Continuity"
   742     "~~/src/HOL/Library/Diagonal_Subsequence"
   743     "~~/src/HOL/Library/Finite_Map"
   744   theories
   745     Probability
   746   document_files "root.tex"
   747 
   748 session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
   749   theories
   750     "Dining_Cryptographers"
   751     "Koepf_Duermuth_Countermeasure"
   752     "Measure_Not_CCC"
   753 
   754 session "HOL-Nominal" in Nominal = HOL +
   755   options [document = false]
   756   theories Nominal
   757 
   758 session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" +
   759   options [document = false]
   760   theories
   761     Class3
   762     CK_Machine
   763     Compile
   764     Contexts
   765     Crary
   766     CR_Takahashi
   767     CR
   768     Fsub
   769     Height
   770     Lambda_mu
   771     Lam_Funs
   772     LocalWeakening
   773     Pattern
   774     SN
   775     SOS
   776     Standardization
   777     Support
   778     Type_Preservation
   779     Weakening
   780     W
   781   theories [quick_and_dirty]
   782     VC_Condition
   783 
   784 session "HOL-Cardinals" (timing) in Cardinals = HOL +
   785   description {*
   786     Ordinals and Cardinals, Full Theories.
   787   *}
   788   options [document = false]
   789   theories
   790     Cardinals
   791     Bounded_Set
   792   document_files
   793     "intro.tex"
   794     "root.tex"
   795     "root.bib"
   796 
   797 session "HOL-Datatype_Examples" (timing) in Datatype_Examples = HOL +
   798   description {*
   799     (Co)datatype Examples.
   800   *}
   801   options [document = false]
   802   theories
   803     Compat
   804     Lambda_Term
   805     Process
   806     TreeFsetI
   807     "Derivation_Trees/Gram_Lang"
   808     "Derivation_Trees/Parallel"
   809     Koenig
   810     Lift_BNF
   811     Milner_Tofte
   812     Stream_Processor
   813     Misc_Codatatype
   814     Misc_Datatype
   815     Misc_Primcorec
   816     Misc_Primrec
   817 
   818 session "HOL-Corec_Examples" (timing) in Corec_Examples = HOL +
   819   description {*
   820     Corecursion Examples.
   821   *}
   822   options [document = false]
   823   theories
   824     LFilter
   825     Paper_Examples
   826     Stream_Processor
   827     "Tests/Simple_Nesting"
   828   theories [quick_and_dirty]
   829     "Tests/GPV_Bare_Bones"
   830     "Tests/Merge_D"
   831     "Tests/Merge_Poly"
   832     "Tests/Misc_Mono"
   833     "Tests/Misc_Poly"
   834     "Tests/Small_Concrete"
   835     "Tests/Stream_Friends"
   836     "Tests/TLList_Friends"
   837     "Tests/Type_Class"
   838 
   839 session "HOL-Word" (main timing) in Word = HOL +
   840   theories Word
   841   document_files "root.bib" "root.tex"
   842 
   843 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   844   options [document = false]
   845   theories WordExamples
   846 
   847 session "HOL-Statespace" in Statespace = HOL +
   848   theories [skip_proofs = false]
   849     StateSpaceEx
   850   document_files "root.tex"
   851 
   852 session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = HOL +
   853   description {*
   854     Nonstandard analysis.
   855   *}
   856   theories
   857     Nonstandard_Analysis
   858   document_files "root.tex"
   859 
   860 session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
   861   options [document = false]
   862   theories NSPrimes
   863 
   864 session "HOL-Mirabelle" in Mirabelle = HOL +
   865   options [document = false]
   866   theories Mirabelle_Test
   867 
   868 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   869   options [document = false, timeout = 60]
   870   theories Ex
   871 
   872 session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" +
   873   options [document = false, quick_and_dirty]
   874   theories
   875     Boogie
   876     SMT_Examples
   877     SMT_Word_Examples
   878     SMT_Tests
   879   files
   880     "Boogie_Dijkstra.certs"
   881     "Boogie_Max.certs"
   882     "SMT_Examples.certs"
   883     "SMT_Word_Examples.certs"
   884     "VCC_Max.certs"
   885 
   886 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   887   options [document = false]
   888   theories SPARK
   889 
   890 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   891   options [document = false, spark_prv = false]
   892   theories
   893     "Gcd/Greatest_Common_Divisor"
   894 
   895     "Liseq/Longest_Increasing_Subsequence"
   896 
   897     "RIPEMD-160/F"
   898     "RIPEMD-160/Hash"
   899     "RIPEMD-160/K_L"
   900     "RIPEMD-160/K_R"
   901     "RIPEMD-160/R_L"
   902     "RIPEMD-160/Round"
   903     "RIPEMD-160/R_R"
   904     "RIPEMD-160/S_L"
   905     "RIPEMD-160/S_R"
   906 
   907     "Sqrt/Sqrt"
   908   files
   909     "Gcd/greatest_common_divisor/g_c_d.fdl"
   910     "Gcd/greatest_common_divisor/g_c_d.rls"
   911     "Gcd/greatest_common_divisor/g_c_d.siv"
   912     "Liseq/liseq/liseq_length.fdl"
   913     "Liseq/liseq/liseq_length.rls"
   914     "Liseq/liseq/liseq_length.siv"
   915     "RIPEMD-160/rmd/f.fdl"
   916     "RIPEMD-160/rmd/f.rls"
   917     "RIPEMD-160/rmd/f.siv"
   918     "RIPEMD-160/rmd/hash.fdl"
   919     "RIPEMD-160/rmd/hash.rls"
   920     "RIPEMD-160/rmd/hash.siv"
   921     "RIPEMD-160/rmd/k_l.fdl"
   922     "RIPEMD-160/rmd/k_l.rls"
   923     "RIPEMD-160/rmd/k_l.siv"
   924     "RIPEMD-160/rmd/k_r.fdl"
   925     "RIPEMD-160/rmd/k_r.rls"
   926     "RIPEMD-160/rmd/k_r.siv"
   927     "RIPEMD-160/rmd/r_l.fdl"
   928     "RIPEMD-160/rmd/r_l.rls"
   929     "RIPEMD-160/rmd/r_l.siv"
   930     "RIPEMD-160/rmd/round.fdl"
   931     "RIPEMD-160/rmd/round.rls"
   932     "RIPEMD-160/rmd/round.siv"
   933     "RIPEMD-160/rmd/r_r.fdl"
   934     "RIPEMD-160/rmd/r_r.rls"
   935     "RIPEMD-160/rmd/r_r.siv"
   936     "RIPEMD-160/rmd/s_l.fdl"
   937     "RIPEMD-160/rmd/s_l.rls"
   938     "RIPEMD-160/rmd/s_l.siv"
   939     "RIPEMD-160/rmd/s_r.fdl"
   940     "RIPEMD-160/rmd/s_r.rls"
   941     "RIPEMD-160/rmd/s_r.siv"
   942 
   943 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   944   options [show_question_marks = false, spark_prv = false]
   945   theories
   946     Example_Verification
   947     VC_Principles
   948     Reference
   949     Complex_Types
   950   files
   951     "complex_types_app/initialize.fdl"
   952     "complex_types_app/initialize.rls"
   953     "complex_types_app/initialize.siv"
   954     "loop_invariant/proc1.fdl"
   955     "loop_invariant/proc1.rls"
   956     "loop_invariant/proc1.siv"
   957     "loop_invariant/proc2.fdl"
   958     "loop_invariant/proc2.rls"
   959     "loop_invariant/proc2.siv"
   960     "simple_greatest_common_divisor/g_c_d.fdl"
   961     "simple_greatest_common_divisor/g_c_d.rls"
   962     "simple_greatest_common_divisor/g_c_d.siv"
   963   document_files
   964     "complex_types.ads"
   965     "complex_types_app.adb"
   966     "complex_types_app.ads"
   967     "Gcd.adb"
   968     "Gcd.ads"
   969     "intro.tex"
   970     "loop_invariant.adb"
   971     "loop_invariant.ads"
   972     "root.bib"
   973     "root.tex"
   974     "Simple_Gcd.adb"
   975     "Simple_Gcd.ads"
   976 
   977 session "HOL-Mutabelle" in Mutabelle = HOL +
   978   options [document = false]
   979   theories MutabelleExtra
   980 
   981 session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = HOL +
   982   options [document = false]
   983   theories
   984     Quickcheck_Examples
   985     Quickcheck_Lattice_Examples
   986     Completeness
   987     Quickcheck_Interfaces
   988     Quickcheck_Nesting_Example
   989   theories [condition = ISABELLE_GHC]
   990     Hotel_Example
   991     Quickcheck_Narrowing_Examples
   992 
   993 session "HOL-Quotient_Examples" (timing) in Quotient_Examples = HOL +
   994   description {*
   995     Author:     Cezary Kaliszyk and Christian Urban
   996   *}
   997   options [document = false]
   998   theories
   999     DList
  1000     Quotient_FSet
  1001     Quotient_Int
  1002     Quotient_Message
  1003     Lift_FSet
  1004     Lift_Set
  1005     Lift_Fun
  1006     Quotient_Rat
  1007     Lift_DList
  1008     Int_Pow
  1009     Lifting_Code_Dt_Test
  1010 
  1011 session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = HOL +
  1012   options [document = false]
  1013   theories
  1014     Examples
  1015     Predicate_Compile_Tests
  1016     Predicate_Compile_Quickcheck_Examples
  1017     Specialisation_Examples
  1018     IMP_1
  1019     IMP_2
  1020     (* FIXME since 21-Jul-2011
  1021     Hotel_Example_Small_Generator *)
  1022     IMP_3
  1023     IMP_4
  1024   theories [condition = ISABELLE_SWIPL]
  1025     Code_Prolog_Examples
  1026     Context_Free_Grammar_Example
  1027     Hotel_Example_Prolog
  1028     Lambda_Example
  1029     List_Examples
  1030   theories [condition = ISABELLE_SWIPL, quick_and_dirty]
  1031     Reg_Exp_Example
  1032 
  1033 session HOLCF (main timing) in HOLCF = HOL +
  1034   description {*
  1035     Author:     Franz Regensburger
  1036     Author:     Brian Huffman
  1037 
  1038     HOLCF -- a semantic extension of HOL by the LCF logic.
  1039   *}
  1040   theories [document = false]
  1041     "~~/src/HOL/Library/Nat_Bijection"
  1042     "~~/src/HOL/Library/Countable"
  1043   theories
  1044     Plain_HOLCF
  1045     Fixrec
  1046     HOLCF
  1047   document_files "root.tex"
  1048 
  1049 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
  1050   theories
  1051     Domain_ex
  1052     Fixrec_ex
  1053     New_Domain
  1054   document_files "root.tex"
  1055 
  1056 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
  1057   options [document = false]
  1058   theories HOLCF_Library
  1059 
  1060 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
  1061   description {*
  1062     IMP -- A WHILE-language and its Semantics.
  1063 
  1064     This is the HOLCF-based denotational semantics of a simple WHILE-language.
  1065   *}
  1066   options [document = false]
  1067   theories HoareEx
  1068   document_files "root.tex"
  1069 
  1070 session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
  1071   description {*
  1072     Miscellaneous examples for HOLCF.
  1073   *}
  1074   options [document = false]
  1075   theories
  1076     Dnat
  1077     Dagstuhl
  1078     Focus_ex
  1079     Fix2
  1080     Hoare
  1081     Concurrency_Monad
  1082     Loop
  1083     Powerdomain_ex
  1084     Domain_Proofs
  1085     Letrec
  1086     Pattern_Match
  1087 
  1088 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
  1089   description {*
  1090     FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
  1091 
  1092     For introductions to FOCUS, see
  1093 
  1094     "The Design of Distributed Systems - An Introduction to FOCUS"
  1095     http://www4.in.tum.de/publ/html.php?e=2
  1096 
  1097     "Specification and Refinement of a Buffer of Length One"
  1098     http://www4.in.tum.de/publ/html.php?e=15
  1099 
  1100     "Specification and Development of Interactive Systems: Focus on Streams,
  1101     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
  1102   *}
  1103   options [document = false]
  1104   theories
  1105     Fstreams
  1106     FOCUS
  1107     Buffer_adm
  1108 
  1109 session IOA (timing) in "HOLCF/IOA" = HOLCF +
  1110   description {*
  1111     Author:     Olaf Mueller
  1112     Copyright   1997 TU München
  1113 
  1114     A formalization of I/O automata in HOLCF.
  1115 
  1116     The distribution contains simulation relations, temporal logic, and an
  1117     abstraction theory. Everything is based upon a domain-theoretic model of
  1118     finite and infinite sequences.
  1119   *}
  1120   options [document = false]
  1121   theories "Abstraction"
  1122 
  1123 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  1124   description {*
  1125     Author:     Olaf Mueller
  1126 
  1127     The Alternating Bit Protocol performed in I/O-Automata.
  1128   *}
  1129   options [document = false]
  1130   theories
  1131     Correctness
  1132     Spec
  1133 
  1134 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
  1135   description {*
  1136     Author:     Tobias Nipkow & Konrad Slind
  1137 
  1138     A network transmission protocol, performed in the
  1139     I/O automata formalization by Olaf Mueller.
  1140   *}
  1141   options [document = false]
  1142   theories Correctness
  1143 
  1144 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
  1145   description {*
  1146     Author:     Olaf Mueller
  1147 
  1148     Memory storage case study.
  1149   *}
  1150   options [document = false]
  1151   theories Correctness
  1152 
  1153 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
  1154   description {*
  1155     Author:     Olaf Mueller
  1156   *}
  1157   options [document = false]
  1158   theories
  1159     TrivEx
  1160     TrivEx2