src/HOL/ROOT

Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)

chapter HOL

session HOL (main) = Pure +
  description {*
    Classical Higher-order Logic.
  *}
  global_theories
    Main
    Complex_Main
  files
    "Tools/Quickcheck/Narrowing_Engine.hs"
    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
  document_files
    "root.bib"
    "root.tex"

session "HOL-Proofs" (timing) = Pure +
  description {*
    HOL-Main with explicit proof terms.
  *}
  options [document = false, quick_and_dirty = false]
  theories Proofs (*sequential change of global flag!*)
  theories List
  theories [checkpoint] "~~/src/HOL/Library/Old_Datatype"
  files
    "Tools/Quickcheck/Narrowing_Engine.hs"
    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"

session "HOL-Library" (main timing) in Library = HOL +
  description {*
    Classical Higher-order Logic -- batteries included.
  *}
  theories
    Library
    Nonpos_Ints
    Periodic_Fun
    Polynomial_Factorial
    Predicate_Compile_Quickcheck
    Prefix_Order
    Rewrite
    (*conflicting type class instantiations*)
    List_lexord
    Sublist_Order
    Product_Lexorder
    Product_Order
    Finite_Lattice
    (*data refinements and dependent applications*)
    AList_Mapping
    Code_Binary_Nat
    Code_Char
    Code_Prolog
    Code_Real_Approx_By_Float
    Code_Target_Numeral
    DAList
    DAList_Multiset
    RBT_Mapping
    RBT_Set
    (*legacy tools*)
    Refute
    Old_Datatype
    Old_Recdef
    Old_SMT
  document_files "root.bib" "root.tex"

session "HOL-Hahn_Banach" in Hahn_Banach = HOL +
  description {*
    Author:     Gertrud Bauer, TU Munich

    The Hahn-Banach theorem for real vector spaces.

    This is the proof of the Hahn-Banach theorem for real vectorspaces,
    following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach
    theorem is one of the fundamental theorems of functional analysis. It is a
    conclusion of Zorn's lemma.

    Two different formaulations of the theorem are presented, one for general
    real vectorspaces and its application to normed vectorspaces.

    The theorem says, that every continous linearform, defined on arbitrary
    subspaces (not only one-dimensional subspaces), can be extended to a
    continous linearform on the whole vectorspace.
  *}
  theories Hahn_Banach
  document_files "root.bib" "root.tex"

session "HOL-Induct" in Induct = HOL +
  description {*
    Examples of (Co)Inductive Definitions.

    Comb proves the Church-Rosser theorem for combinators (see
    http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz).

    Mutil is the famous Mutilated Chess Board problem (see
    http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz).

    PropLog proves the completeness of a formalization of propositional logic
    (see
    http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz).

    Exp demonstrates the use of iterated inductive definitions to reason about
    mutually recursive relations.
  *}
  theories [document = false]
    "~~/src/HOL/Library/Old_Datatype"
  theories [quick_and_dirty]
    Common_Patterns
  theories
    Nested_Datatype
    QuoDataType
    QuoNestedDataType
    Term
    SList
    ABexp
    Tree
    Ordinals
    Sigma_Algebra
    Comb
    PropLog
    Com
  document_files "root.tex"

session "HOL-IMP" (timing) in IMP = HOL +
  options [document_variants = document]
  theories [document = false]
    "~~/src/HOL/Library/While_Combinator"
    "~~/src/HOL/Library/Char_ord"
    "~~/src/HOL/Library/List_lexord"
    "~~/src/HOL/Library/Quotient_List"
    "~~/src/HOL/Library/Extended"
  theories
    BExp
    ASM
    Finite_Reachable
    Denotational
    Compiler2
    Poly_Types
    Sec_Typing
    Sec_TypingT
    Def_Init_Big
    Def_Init_Small
    Fold
    Live
    Live_True
    Hoare_Examples
    Hoare_Sound_Complete
    VCG
    Hoare_Total
    VCG_Total_EX
    Collecting1
    Collecting_Examples
    Abs_Int_Tests
    Abs_Int1_parity
    Abs_Int1_const
    Abs_Int3
    "Abs_Int_ITP/Abs_Int1_parity_ITP"
    "Abs_Int_ITP/Abs_Int1_const_ITP"
    "Abs_Int_ITP/Abs_Int3_ITP"
    Procs_Dyn_Vars_Dyn
    Procs_Stat_Vars_Dyn
    Procs_Stat_Vars_Stat
    C_like
    OO
  document_files "root.bib" "root.tex"

session "HOL-IMPP" in IMPP = HOL +
  description {*
    Author:     David von Oheimb
    Copyright   1999 TUM

    IMPP -- An imperative language with procedures.

    This is an extension of IMP with local variables and mutually recursive
    procedures. For documentation see "Hoare Logic for Mutual Recursion and
    Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
  *}
  options [document = false]
  theories EvenOdd

session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
  options [document_variants = document]
  theories [document = false]
    "Less_False"
    "~~/src/HOL/Library/Multiset"
    "~~/src/HOL/Library/Float"
  theories
    Balance
    Tree_Map
    AVL_Map
    RBT_Map
    Tree23_Map
    Tree234_Map
    Brother12_Map
    AA_Map
    Splay_Map
    Leftist_Heap
  document_files "root.tex" "root.bib"

session "HOL-Import" in Import = HOL +
  theories HOL_Light_Maps
  theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import

session "HOL-Number_Theory" (timing) in Number_Theory = HOL +
  description {*
    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
    Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
  *}
  theories [document = false]
    "~~/src/HOL/Library/FuncSet"
    "~~/src/HOL/Library/Multiset"
    "~~/src/HOL/Algebra/Ring"
    "~~/src/HOL/Algebra/FiniteProduct"
  theories
    Pocklington
    Gauss
    Number_Theory
    Euclidean_Algorithm
    Factorial_Ring
  document_files
    "root.tex"

session "HOL-Hoare" in Hoare = HOL +
  description {*
    Verification of imperative programs (verification conditions are generated
    automatically from pre/post conditions and loop invariants).
  *}
  theories Hoare
  document_files "root.bib" "root.tex"

session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL +
  description {*
    Verification of shared-variable imperative programs a la Owicki-Gries.
    (verification conditions are generated automatically).
  *}
  theories Hoare_Parallel
  document_files "root.bib" "root.tex"

session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
  options [document = false, browser_info = false]
  theories
    Generate
    Generate_Binary_Nat
    Generate_Target_Nat
    Generate_Efficient_Datastructures
    Generate_Pretty_Char
  theories [condition = "ISABELLE_GHC"]
    Code_Test_GHC
  theories [condition = "ISABELLE_MLTON"]
    Code_Test_MLton
  theories [condition = "ISABELLE_OCAMLC"]
    Code_Test_OCaml
  theories [condition = "ISABELLE_POLYML"]
    Code_Test_PolyML
  theories [condition = "ISABELLE_SCALA"]
    Code_Test_Scala
  theories [condition = "ISABELLE_SMLNJ"]
    Code_Test_SMLNJ

session "HOL-Metis_Examples" (timing) in Metis_Examples = HOL +
  description {*
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Author:     Jasmin Blanchette, TU Muenchen

    Testing Metis and Sledgehammer.
  *}
  options [document = false]
  theories
    Abstraction
    Big_O
    Binary_Tree
    Clausification
    Message
    Proxies
    Tarski
    Trans_Closure
    Sets

session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL +
  description {*
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2009
  *}
  options [document = false]
  theories [quick_and_dirty] Nitpick_Examples

session "HOL-Algebra" (main timing) in Algebra = HOL +
  description {*
    Author: Clemens Ballarin, started 24 September 1999

    The Isabelle Algebraic Library.
  *}
  theories [document = false]
    (* Preliminaries from set and number theory *)
    "~~/src/HOL/Library/FuncSet"
    "~~/src/HOL/Number_Theory/Primes"
    "~~/src/HOL/Library/Permutation"
  theories
    (*** New development, based on explicit structures ***)
    (* Groups *)
    FiniteProduct        (* Product operator for commutative groups *)
    Sylow                (* Sylow's theorem *)
    Bij                  (* Automorphism Groups *)

    (* Rings *)
    Divisibility         (* Rings *)
    IntRing              (* Ideals and residue classes *)
    UnivPoly             (* Polynomials *)
  document_files "root.bib" "root.tex"

session "HOL-Auth" (timing) in Auth = HOL +
  description {*
    A new approach to verifying authentication protocols.
  *}
  theories
    Auth_Shared
    Auth_Public
    "Smartcard/Auth_Smartcard"
    "Guard/Auth_Guard_Shared"
    "Guard/Auth_Guard_Public"
  document_files "root.tex"

session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" +
  description {*
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

    Verifying security protocols using Chandy and Misra's UNITY formalism.
  *}
  theories
    (*Basic meta-theory*)
    "UNITY_Main"

    (*Simple examples: no composition*)
    "Simple/Deadlock"
    "Simple/Common"
    "Simple/Network"
    "Simple/Token"
    "Simple/Channel"
    "Simple/Lift"
    "Simple/Mutex"
    "Simple/Reach"
    "Simple/Reachability"

    (*Verifying security protocols using UNITY*)
    "Simple/NSP_Bad"

    (*Example of composition*)
    "Comp/Handshake"

    (*Universal properties examples*)
    "Comp/Counter"
    "Comp/Counterc"
    "Comp/Priority"

    "Comp/TimerArray"
    "Comp/Progress"

    "Comp/Alloc"
    "Comp/AllocImpl"
    "Comp/Client"

    (*obsolete*)
    "ELT"
  document_files "root.tex"

session "HOL-Unix" in Unix = HOL +
  options [print_mode = "no_brackets,no_type_brackets"]
  theories Unix
  document_files "root.bib" "root.tex"

session "HOL-ZF" in ZF = HOL +
  theories MainZF Games
  document_files "root.tex"

session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
  options [print_mode = "iff,no_brackets"]
  theories [document = false]
    "~~/src/HOL/Library/Countable"
    "~~/src/HOL/Library/Monad_Syntax"
    "~~/src/HOL/Library/LaTeXsugar"
  theories Imperative_HOL_ex
  document_files "root.bib" "root.tex"

session "HOL-Decision_Procs" (timing) in Decision_Procs = HOL +
  description {*
    Various decision procedures, typically involving reflection.
  *}
  options [document = false]
  theories Decision_Procs

session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
  options [document = false, parallel_proofs = 0]
  theories
    Hilbert_Classical
    Proof_Terms
    XML_Data

session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" +
  description {*
    Examples for program extraction in Higher-Order Logic.
  *}
  options [parallel_proofs = 0, quick_and_dirty = false]
  theories [document = false]
    "~~/src/HOL/Library/Code_Target_Numeral"
    "~~/src/HOL/Library/Monad_Syntax"
    "~~/src/HOL/Number_Theory/Primes"
    "~~/src/HOL/Library/State_Monad"
  theories
    Greatest_Common_Divisor
    Warshall
    Higman_Extraction
    Pigeonhole
    Euclid
  document_files "root.bib" "root.tex"

session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" +
  description {*
    Lambda Calculus in de Bruijn's Notation.

    This session defines lambda-calculus terms with de Bruijn indixes and
    proves confluence of beta, eta and beta+eta.

    The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
    theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
  *}
  options [print_mode = "no_brackets",
    parallel_proofs = 0, quick_and_dirty = false]
  theories [document = false]
    "~~/src/HOL/Library/Code_Target_Int"
  theories
    Eta
    StrongNorm
    Standardization
    WeakNorm
  document_files "root.bib" "root.tex"

session "HOL-Prolog" in Prolog = HOL +
  description {*
    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)

    A bare-bones implementation of Lambda-Prolog.

    This is a simple exploratory implementation of Lambda-Prolog in HOL,
    including some minimal examples (in Test.thy) and a more typical example of
    a little functional language and its type system.
  *}
  options [document = false]
  theories Test Type

session "HOL-MicroJava" (timing) in MicroJava = HOL +
  description {*
    Formalization of a fragment of Java, together with a corresponding virtual
    machine and a specification of its bytecode verifier and a lightweight
    bytecode verifier, including proofs of type-safety.
  *}
  theories [document = false]
    "~~/src/HOL/Library/While_Combinator"
  theories
    MicroJava
  document_files
    "introduction.tex"
    "root.bib"
    "root.tex"

session "HOL-NanoJava" in NanoJava = HOL +
  description {*
    Hoare Logic for a tiny fragment of Java.
  *}
  theories Example
  document_files "root.bib" "root.tex"

session "HOL-Bali" (timing) in Bali = HOL +
  theories
    AxExample
    AxSound
    AxCompl
    Trans
    TypeSafe
  document_files "root.tex"

session "HOL-IOA" in IOA = HOL +
  description {*
    Author:     Tobias Nipkow and Konrad Slind and Olaf Müller
    Copyright   1994--1996  TU Muenchen

    The meta-theory of I/O-Automata in HOL. This formalization has been
    significantly changed and extended, see HOLCF/IOA. There are also the
    proofs of two communication protocols which formerly have been here.

    @inproceedings{Nipkow-Slind-IOA,
    author={Tobias Nipkow and Konrad Slind},
    title={{I/O} Automata in {Isabelle/HOL}},
    booktitle={Proc.\ TYPES Workshop 1994},
    publisher=Springer,
    series=LNCS,
    note={To appear}}
    ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz

    and

    @inproceedings{Mueller-Nipkow,
    author={Olaf M\"uller and Tobias Nipkow},
    title={Combining Model Checking and Deduction for {I/O}-Automata},
    booktitle={Proc.\ TACAS Workshop},
    organization={Aarhus University, BRICS report},
    year=1995}
    ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
  *}
  options [document = false]
  theories Solve

session "HOL-Lattice" in Lattice = HOL +
  description {*
    Author:     Markus Wenzel, TU Muenchen

    Basic theory of lattices and orders.
  *}
  theories CompleteLattice
  document_files "root.tex"

session "HOL-ex" in ex = HOL +
  description {*
    Miscellaneous examples for Higher-Order Logic.
  *}
  theories [document = false]
    "~~/src/HOL/Library/State_Monad"
    Code_Binary_Nat_examples
    "~~/src/HOL/Library/FuncSet"
    Eval_Examples
    Normalization_by_Evaluation
    Hebrew
    Chinese
    Serbian
    "~~/src/HOL/Library/Refute"
    "~~/src/HOL/Library/Transitive_Closure_Table"
    Cartouche_Examples
  theories
    Commands
    Adhoc_Overloading_Examples
    Iff_Oracle
    Coercion_Examples
    Abstract_NAT
    Guess
    Functions
    Induction_Schema
    LocaleTest2
    Records
    While_Combinator_Example
    MonoidGroup
    BinEx
    Hex_Bin_Examples
    Antiquote
    Multiquote
    PER
    NatSum
    ThreeDivides
    Cubic_Quartic
    Pythagoras
    Intuitionistic
    CTL
    Arith_Examples
    Tree23
    Bubblesort
    MergeSort
    Lagrange
    Groebner_Examples
    Unification
    Primrec
    Tarski
    Classical
    Set_Theory
    Termination
    Coherent
    PresburgerEx
    Reflection_Examples
    Sqrt
    Sqrt_Script
    Transfer_Debug
    Transfer_Ex
    Transfer_Int_Nat
    Transitive_Closure_Table_Ex
    HarmonicSeries
    Refute_Examples
    Execute_Choice
    Gauge_Integration
    Dedekind_Real
    Quicksort
    Birthday_Paradox
    List_to_Set_Comprehension_Examples
    Seq
    Simproc_Tests
    Executable_Relation
    FinFunPred
    Set_Comprehension_Pointfree_Examples
    Parallel_Example
    IArray_Examples
    Simps_Case_Conv_Examples
    ML
    Rewrite_Examples
    SAT_Examples
    SOS
    SOS_Cert
    Ballot
    Erdoes_Szekeres
    Sum_of_Powers
    Sudoku
    Code_Timing
    Perm_Fragments
    Argo_Examples
    Word_Type
  theories [skip_proofs = false]
    Meson_Test
  document_files "root.bib" "root.tex"

session "HOL-Isar_Examples" in Isar_Examples = HOL +
  description {*
    Miscellaneous Isabelle/Isar examples.
  *}
  options [quick_and_dirty]
  theories [document = false]
    "~~/src/HOL/Library/Lattice_Syntax"
    "../Number_Theory/Primes"
  theories
    Knaster_Tarski
    Peirce
    Drinker
    Cantor
    Structured_Statements
    Basic_Logic
    Expr_Compiler
    Fibonacci
    Group
    Group_Context
    Group_Notepad
    Hoare_Ex
    Mutilated_Checkerboard
    Puzzle
    Summation
    First_Order_Logic
    Higher_Order_Logic
  document_files
    "root.bib"
    "root.tex"

session "HOL-Eisbach" in Eisbach = HOL +
  description {*
    The Eisbach proof method language and "match" method.
  *}
  theories
    Eisbach
    Tests
    Examples
    Examples_FOL

session "HOL-SET_Protocol" (timing) in SET_Protocol = HOL +
  description {*
    Verification of the SET Protocol.
  *}
  theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
  theories SET_Protocol
  document_files "root.tex"

session "HOL-Matrix_LP" in Matrix_LP = HOL +
  description {*
    Two-dimensional matrices and linear programming.
  *}
  theories Cplex
  document_files "root.tex"

session "HOL-TLA" in TLA = HOL +
  description {*
    Lamport's Temporal Logic of Actions.
  *}
  options [document = false]
  theories TLA

session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
  options [document = false]
  theories Inc

session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
  options [document = false]
  theories DBuffer

session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
  options [document = false]
  theories MemoryImplementation

session "HOL-TPTP" in TPTP = HOL +
  description {*
    Author:     Jasmin Blanchette, TU Muenchen
    Author:     Nik Sultana, University of Cambridge
    Copyright   2011

    TPTP-related extensions.
  *}
  options [document = false]
  theories
    ATP_Theory_Export
    MaSh_Eval
    TPTP_Interpret
    THF_Arith
    TPTP_Proof_Reconstruction
  theories
    ATP_Problem_Import

session "HOL-Analysis" (main timing) in Analysis = HOL +
  theories
    Analysis
  document_files
    "root.tex"

session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" +
  theories
    Approximations

session "HOL-Probability" (timing) in "Probability" = "HOL-Analysis" +
  theories [document = false]
    "~~/src/HOL/Library/Countable"
    "~~/src/HOL/Library/Permutation"
    "~~/src/HOL/Library/Order_Continuity"
    "~~/src/HOL/Library/Diagonal_Subsequence"
    "~~/src/HOL/Library/Finite_Map"
  theories
    Probability
  document_files "root.tex"

session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
  theories
    "Dining_Cryptographers"
    "Koepf_Duermuth_Countermeasure"
    "Measure_Not_CCC"

session "HOL-Nominal" in Nominal = HOL +
  options [document = false]
  theories Nominal

session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" +
  options [document = false]
  theories
    Class3
    CK_Machine
    Compile
    Contexts
    Crary
    CR_Takahashi
    CR
    Fsub
    Height
    Lambda_mu
    Lam_Funs
    LocalWeakening
    Pattern
    SN
    SOS
    Standardization
    Support
    Type_Preservation
    Weakening
    W
  theories [quick_and_dirty]
    VC_Condition

session "HOL-Cardinals" (timing) in Cardinals = HOL +
  description {*
    Ordinals and Cardinals, Full Theories.
  *}
  options [document = false]
  theories
    Cardinals
    Bounded_Set
  document_files
    "intro.tex"
    "root.tex"
    "root.bib"

session "HOL-Datatype_Examples" (timing) in Datatype_Examples = HOL +
  description {*
    (Co)datatype Examples.
  *}
  options [document = false]
  theories
    Compat
    Lambda_Term
    Process
    TreeFsetI
    "Derivation_Trees/Gram_Lang"
    "Derivation_Trees/Parallel"
    Koenig
    Lift_BNF
    Milner_Tofte
    Stream_Processor
    Misc_Codatatype
    Misc_Datatype
    Misc_Primcorec
    Misc_Primrec

session "HOL-Corec_Examples" (timing) in Corec_Examples = HOL +
  description {*
    Corecursion Examples.
  *}
  options [document = false]
  theories
    LFilter
    Paper_Examples
    Stream_Processor
    "Tests/Simple_Nesting"
  theories [quick_and_dirty]
    "Tests/GPV_Bare_Bones"
    "Tests/Merge_D"
    "Tests/Merge_Poly"
    "Tests/Misc_Mono"
    "Tests/Misc_Poly"
    "Tests/Small_Concrete"
    "Tests/Stream_Friends"
    "Tests/TLList_Friends"
    "Tests/Type_Class"

session "HOL-Word" (main timing) in Word = HOL +
  theories Word
  document_files "root.bib" "root.tex"

session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
  options [document = false]
  theories WordExamples

session "HOL-Statespace" in Statespace = HOL +
  theories [skip_proofs = false]
    StateSpaceEx
  document_files "root.tex"

session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = HOL +
  description {*
    Nonstandard analysis.
  *}
  theories
    Nonstandard_Analysis
  document_files "root.tex"

session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
  options [document = false]
  theories NSPrimes

session "HOL-Mirabelle" in Mirabelle = HOL +
  options [document = false]
  theories Mirabelle_Test

session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
  options [document = false, timeout = 60]
  theories Ex

session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" +
  options [document = false, quick_and_dirty]
  theories
    Boogie
    SMT_Examples
    SMT_Word_Examples
    SMT_Tests
  files
    "Boogie_Dijkstra.certs"
    "Boogie_Max.certs"
    "SMT_Examples.certs"
    "SMT_Word_Examples.certs"
    "VCC_Max.certs"

session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
  options [document = false]
  theories SPARK

session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
  options [document = false, spark_prv = false]
  theories
    "Gcd/Greatest_Common_Divisor"

    "Liseq/Longest_Increasing_Subsequence"

    "RIPEMD-160/F"
    "RIPEMD-160/Hash"
    "RIPEMD-160/K_L"
    "RIPEMD-160/K_R"
    "RIPEMD-160/R_L"
    "RIPEMD-160/Round"
    "RIPEMD-160/R_R"
    "RIPEMD-160/S_L"
    "RIPEMD-160/S_R"

    "Sqrt/Sqrt"
  files
    "Gcd/greatest_common_divisor/g_c_d.fdl"
    "Gcd/greatest_common_divisor/g_c_d.rls"
    "Gcd/greatest_common_divisor/g_c_d.siv"
    "Liseq/liseq/liseq_length.fdl"
    "Liseq/liseq/liseq_length.rls"
    "Liseq/liseq/liseq_length.siv"
    "RIPEMD-160/rmd/f.fdl"
    "RIPEMD-160/rmd/f.rls"
    "RIPEMD-160/rmd/f.siv"
    "RIPEMD-160/rmd/hash.fdl"
    "RIPEMD-160/rmd/hash.rls"
    "RIPEMD-160/rmd/hash.siv"
    "RIPEMD-160/rmd/k_l.fdl"
    "RIPEMD-160/rmd/k_l.rls"
    "RIPEMD-160/rmd/k_l.siv"
    "RIPEMD-160/rmd/k_r.fdl"
    "RIPEMD-160/rmd/k_r.rls"
    "RIPEMD-160/rmd/k_r.siv"
    "RIPEMD-160/rmd/r_l.fdl"
    "RIPEMD-160/rmd/r_l.rls"
    "RIPEMD-160/rmd/r_l.siv"
    "RIPEMD-160/rmd/round.fdl"
    "RIPEMD-160/rmd/round.rls"
    "RIPEMD-160/rmd/round.siv"
    "RIPEMD-160/rmd/r_r.fdl"
    "RIPEMD-160/rmd/r_r.rls"
    "RIPEMD-160/rmd/r_r.siv"
    "RIPEMD-160/rmd/s_l.fdl"
    "RIPEMD-160/rmd/s_l.rls"
    "RIPEMD-160/rmd/s_l.siv"
    "RIPEMD-160/rmd/s_r.fdl"
    "RIPEMD-160/rmd/s_r.rls"
    "RIPEMD-160/rmd/s_r.siv"

session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
  options [show_question_marks = false, spark_prv = false]
  theories
    Example_Verification
    VC_Principles
    Reference
    Complex_Types
  files
    "complex_types_app/initialize.fdl"
    "complex_types_app/initialize.rls"
    "complex_types_app/initialize.siv"
    "loop_invariant/proc1.fdl"
    "loop_invariant/proc1.rls"
    "loop_invariant/proc1.siv"
    "loop_invariant/proc2.fdl"
    "loop_invariant/proc2.rls"
    "loop_invariant/proc2.siv"
    "simple_greatest_common_divisor/g_c_d.fdl"
    "simple_greatest_common_divisor/g_c_d.rls"
    "simple_greatest_common_divisor/g_c_d.siv"
  document_files
    "complex_types.ads"
    "complex_types_app.adb"
    "complex_types_app.ads"
    "Gcd.adb"
    "Gcd.ads"
    "intro.tex"
    "loop_invariant.adb"
    "loop_invariant.ads"
    "root.bib"
    "root.tex"
    "Simple_Gcd.adb"
    "Simple_Gcd.ads"

session "HOL-Mutabelle" in Mutabelle = HOL +
  options [document = false]
  theories MutabelleExtra

session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = HOL +
  options [document = false]
  theories
    Quickcheck_Examples
    Quickcheck_Lattice_Examples
    Completeness
    Quickcheck_Interfaces
    Quickcheck_Nesting_Example
  theories [condition = ISABELLE_GHC]
    Hotel_Example
    Quickcheck_Narrowing_Examples

session "HOL-Quotient_Examples" (timing) in Quotient_Examples = HOL +
  description {*
    Author:     Cezary Kaliszyk and Christian Urban
  *}
  options [document = false]
  theories
    DList
    Quotient_FSet
    Quotient_Int
    Quotient_Message
    Lift_FSet
    Lift_Set
    Lift_Fun
    Quotient_Rat
    Lift_DList
    Int_Pow
    Lifting_Code_Dt_Test

session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = HOL +
  options [document = false]
  theories
    Examples
    Predicate_Compile_Tests
    Predicate_Compile_Quickcheck_Examples
    Specialisation_Examples
    IMP_1
    IMP_2
    (* FIXME since 21-Jul-2011
    Hotel_Example_Small_Generator *)
    IMP_3
    IMP_4
  theories [condition = ISABELLE_SWIPL]
    Code_Prolog_Examples
    Context_Free_Grammar_Example
    Hotel_Example_Prolog
    Lambda_Example
    List_Examples
  theories [condition = ISABELLE_SWIPL, quick_and_dirty]
    Reg_Exp_Example

session HOLCF (main timing) in HOLCF = HOL +
  description {*
    Author:     Franz Regensburger
    Author:     Brian Huffman

    HOLCF -- a semantic extension of HOL by the LCF logic.
  *}
  theories [document = false]
    "~~/src/HOL/Library/Nat_Bijection"
    "~~/src/HOL/Library/Countable"
  theories
    Plain_HOLCF
    Fixrec
    HOLCF
  document_files "root.tex"

session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
  theories
    Domain_ex
    Fixrec_ex
    New_Domain
  document_files "root.tex"

session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
  options [document = false]
  theories HOLCF_Library

session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
  description {*
    IMP -- A WHILE-language and its Semantics.

    This is the HOLCF-based denotational semantics of a simple WHILE-language.
  *}
  options [document = false]
  theories HoareEx
  document_files "root.tex"

session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
  description {*
    Miscellaneous examples for HOLCF.
  *}
  options [document = false]
  theories
    Dnat
    Dagstuhl
    Focus_ex
    Fix2
    Hoare
    Concurrency_Monad
    Loop
    Powerdomain_ex
    Domain_Proofs
    Letrec
    Pattern_Match

session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
  description {*
    FOCUS: a theory of stream-processing functions Isabelle/HOLCF.

    For introductions to FOCUS, see

    "The Design of Distributed Systems - An Introduction to FOCUS"
    http://www4.in.tum.de/publ/html.php?e=2

    "Specification and Refinement of a Buffer of Length One"
    http://www4.in.tum.de/publ/html.php?e=15

    "Specification and Development of Interactive Systems: Focus on Streams,
    Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
  *}
  options [document = false]
  theories
    Fstreams
    FOCUS
    Buffer_adm

session IOA (timing) in "HOLCF/IOA" = HOLCF +
  description {*
    Author:     Olaf Mueller
    Copyright   1997 TU München

    A formalization of I/O automata in HOLCF.

    The distribution contains simulation relations, temporal logic, and an
    abstraction theory. Everything is based upon a domain-theoretic model of
    finite and infinite sequences.
  *}
  options [document = false]
  theories "Abstraction"

session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  description {*
    Author:     Olaf Mueller

    The Alternating Bit Protocol performed in I/O-Automata.
  *}
  options [document = false]
  theories
    Correctness
    Spec

session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
  description {*
    Author:     Tobias Nipkow & Konrad Slind

    A network transmission protocol, performed in the
    I/O automata formalization by Olaf Mueller.
  *}
  options [document = false]
  theories Correctness

session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
  description {*
    Author:     Olaf Mueller

    Memory storage case study.
  *}
  options [document = false]
  theories Correctness

session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
  description {*
    Author:     Olaf Mueller
  *}
  options [document = false]
  theories
    TrivEx
    TrivEx2