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