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