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