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