src/HOL/ROOT

corrected some confusing terminology / notation

chapter HOL

session HOL (main) = Pure +
  description "
    Classical Higher-order Logic.
  "
  options [strict_facts]
  sessions Tools
  theories
    Main (global)
    Complex_Main (global)
  document_files
    "root.bib"
    "root.tex"

session "HOL-Proofs" (timing) in Proofs = Pure +
  description "
    HOL-Main with explicit proof terms.
  "
  options [quick_and_dirty = false, record_proofs = 2, parallel_limit = 500]
  sessions
    "HOL-Library"
  theories
    "HOL-Library.Realizers"

session "HOL-Library" (main timing) in Library = HOL +
  description "
    Classical Higher-order Logic -- batteries included.
  "
  theories
    Library
    (*conflicting type class instantiations and dependent applications*)
    Finite_Lattice
    List_Lexorder
    Prefix_Order
    Product_Lexorder
    Product_Order
    Subseq_Order
    (*conflicting syntax*)
    Datatype_Records
    (*data refinements and dependent applications*)
    AList_Mapping
    Code_Binary_Nat
    Code_Prolog
    Code_Real_Approx_By_Float
    Code_Target_Numeral
    DAList
    DAList_Multiset
    RBT_Mapping
    RBT_Set
    (*printing modifications*)
    OptionalSugar
    (*prototypic tools*)
    Predicate_Compile_Quickcheck
    (*legacy tools*)
    Old_Datatype
    Old_Recdef
    Realizers
    Refute
  document_files "root.bib" "root.tex"

session "HOL-Analysis" (main timing) in Analysis = HOL +
  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
    document_variants = "document:manual=-proof,-ML,-unimportant"]
  sessions
    "HOL-Library"
    "HOL-Computational_Algebra"
  theories
    Analysis
  document_files
    "root.tex"
    "root.bib"

session "HOL-Complex_Analysis" (main timing) in Complex_Analysis = "HOL-Analysis" +
  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
    document_variants = "document:manual=-proof,-ML,-unimportant"]
  theories
    Complex_Analysis
  document_files
    "root.tex"
    "root.bib"

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

session "HOL-Homology" (timing) in Homology = "HOL-Analysis" +
  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
    document_variants = "document:manual=-proof,-ML,-unimportant"]
  sessions
    "HOL-Algebra"
  theories
    Homology
  document_files
    "root.tex"

session "HOL-Computational_Algebra" (main timing) in "Computational_Algebra" = "HOL-Library" +
  theories
    Computational_Algebra
    (*conflicting type class instantiations and dependent applications*)
    Field_as_Ring

session "HOL-Real_Asymp" in Real_Asymp = HOL +
  sessions
    "HOL-Decision_Procs"
  theories
    Real_Asymp
    Real_Asymp_Approx
    Real_Asymp_Examples

session "HOL-Real_Asymp-Manual" in "Real_Asymp/Manual" = "HOL-Real_Asymp" +
  theories
    Real_Asymp_Doc
  document_files (in "~~/src/Doc")
    "iman.sty"
    "extra.sty"
    "isar.sty"
  document_files
    "root.tex"
    "style.sty"

session "HOL-Hahn_Banach" in Hahn_Banach = "HOL-Library" +
  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.
  "
  sessions
    "HOL-Analysis"
  theories
    Hahn_Banach
  document_files "root.bib" "root.tex"

session "HOL-Induct" in Induct = "HOL-Library" +
  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 [quick_and_dirty]
    Common_Patterns
  theories
    Nested_Datatype
    QuoDataType
    QuoNestedDataType
    Term
    SList
    ABexp
    Infinitely_Branching_Tree
    Ordinals
    Sigma_Algebra
    Comb
    PropLog
    Com
  document_files "root.tex"

session "HOL-IMP" (timing) in IMP = "HOL-Library" +
  options [document_variants = document]
  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
    VCG_Total_EX2
    Collecting1
    Collecting_Examples
    Abs_Int_Tests
    Abs_Int1_parity
    Abs_Int1_const
    Abs_Int3
    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 \<open>
    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" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
  \<close>
  theories EvenOdd

session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
  options [document_variants = document]
  sessions
    "HOL-Number_Theory"
  theories [document = false]
    Less_False
  theories
    Sorting
    Balance
    Tree_Map
    AVL_Map
    RBT_Map
    Tree23_Map
    Tree234_Map
    Brother12_Map
    AA_Map
    Set2_Join_RBT
    Array_Braun
    Trie_Fun
    Trie_Map
    Tries_Binary
    Leftist_Heap
    Binomial_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" (main timing) in Number_Theory = "HOL-Computational_Algebra" +
  description "
    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
    Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
  "
  sessions
    "HOL-Algebra"
  theories
    Number_Theory
  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-Number_Theory" +
  sessions
    "HOL-Data_Structures"
    "HOL-ex"
  theories
    Generate
    Generate_Binary_Nat
    Generate_Target_Nat
    Generate_Efficient_Datastructures
    Code_Lazy_Test
    Code_Test_PolyML
    Code_Test_Scala
  theories [condition = ISABELLE_GHC]
    Code_Test_GHC
  theories [condition = ISABELLE_MLTON]
    Code_Test_MLton
  theories [condition = ISABELLE_OCAMLFIND]
    Code_Test_OCaml
  theories [condition = ISABELLE_SMLNJ]
    Code_Test_SMLNJ

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

    Testing Metis and Sledgehammer.
  "
  sessions
    "HOL-Decision_Procs"
  theories
    Abstraction
    Big_O
    Binary_Tree
    Clausification
    Message
    Proxies
    Tarski
    Trans_Closure
    Sets

session "HOL-Nitpick_Examples" in Nitpick_Examples = "HOL-Library" +
  description "
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2009
  "
  theories [quick_and_dirty] Nitpick_Examples

session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" +
  description "
    Author: Clemens Ballarin, started 24 September 1999, and many others

    The Isabelle Algebraic Library.
  "
  sessions
    "HOL-Cardinals"
  theories
    (* Orders and Lattices *)
    Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
    (* Groups *)
    FiniteProduct        (* Product operator for commutative groups *)
    Sylow                (* Sylow's theorem *)
    Bij                  (* Automorphism Groups *)
    Multiplicative_Group
    Zassenhaus            (* The Zassenhaus lemma *)
    (* Rings *)
    Divisibility         (* Rings *)
    IntRing              (* Ideals and residue classes *)
    UnivPoly             (* Polynomials *)
    (* Main theory *)
    Algebra
  document_files "root.bib" "root.tex"

session "HOL-Auth" (timing) in Auth = "HOL-Library" +
  description "
    A new approach to verifying authentication protocols.
  "
  directories "Smartcard" "Guard"
  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.
  "
  directories "Simple" "Comp"
  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-Library" +
  options [print_mode = "no_brackets,no_type_brackets"]
  theories Unix
  document_files "root.bib" "root.tex"

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

session "HOL-Imperative_HOL" (timing) in Imperative_HOL = "HOL-Library" +
  options [print_mode = "iff,no_brackets"]
  directories "ex"
  theories Imperative_HOL_ex
  document_files "root.bib" "root.tex"

session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" +
  description "
    Various decision procedures, typically involving reflection.
  "
  directories "ex"
  theories
    Decision_Procs

session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
  sessions
    "HOL-Isar_Examples"
  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 [quick_and_dirty = false]
  sessions
    "HOL-Computational_Algebra"
  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 \<open>
    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).
  \<close>
  options [print_mode = "no_brackets", quick_and_dirty = false]
  sessions
    "HOL-Library"
  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.
  "
  theories Test Type

session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" +
  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.
  "
  sessions
    "HOL-Eisbach"
  directories "BV" "Comp" "DFA" "J" "JVM"
  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-Library" +
  theories
    AxExample
    AxSound
    AxCompl
    Trans
    TypeSafe
  document_files "root.tex"

session "HOL-IOA" in IOA = HOL +
  description \<open>
    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
  \<close>
  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" (timing) in ex = "HOL-Number_Theory" +
  description "
    Miscellaneous examples for Higher-Order Logic.
  "
  theories
    Adhoc_Overloading_Examples
    Antiquote
    Argo_Examples
    Arith_Examples
    Ballot
    BinEx
    Birthday_Paradox
    Bit_Lists
    Bubblesort
    CTL
    Cartouche_Examples
    Case_Product
    Chinese
    Classical
    Code_Binary_Nat_examples
    Code_Lazy_Demo
    Code_Timing
    Coercion_Examples
    Coherent
    Commands
    Computations
    Conditional_Parametricity_Examples
    Cubic_Quartic
    Datatype_Record_Examples
    Dedekind_Real
    Erdoes_Szekeres
    Eval_Examples
    Executable_Relation
    Execute_Choice
    Functions
    Function_Growth
    Gauge_Integration
    Groebner_Examples
    Guess
    HarmonicSeries
    Hebrew
    Hex_Bin_Examples
    IArray_Examples
    Iff_Oracle
    Induction_Schema
    Intuitionistic
    Join_Theory
    Lagrange
    List_to_Set_Comprehension_Examples
    LocaleTest2
    "ML"
    MergeSort
    MonoidGroup
    Multiquote
    NatSum
    Normalization_by_Evaluation
    PER
    Parallel_Example
    Peano_Axioms
    Perm_Fragments
    PresburgerEx
    Primrec
    Pythagoras
    Quicksort
    Radix_Sort
    Records
    Reflection_Examples
    Refute_Examples
    Residue_Ring
    Rewrite_Examples
    SOS
    SOS_Cert
    Seq
    Serbian
    Set_Comprehension_Pointfree_Examples
    Set_Theory
    Simproc_Tests
    Simps_Case_Conv_Examples
    Sketch_and_Explore
    Sorting_Algorithms_Examples
    Sqrt
    Sqrt_Script
    Sudoku
    Sum_of_Powers
    Tarski
    Termination
    ThreeDivides
    Transfer_Debug
    Transfer_Int_Nat
    Transitive_Closure_Table_Ex
    Tree23
    Triangular_Numbers
    Unification
    While_Combinator_Example
    Word
    veriT_Preprocessing
  theories [skip_proofs = false]
    SAT_Examples
    Meson_Test

session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" +
  description "
    Miscellaneous Isabelle/Isar examples.
  "
  options [quick_and_dirty]
  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 \<open>
    The Eisbach proof method language and "match" method.
  \<close>
  sessions
    FOL
    "HOL-Analysis"
  theories
    Eisbach
    Tests
    Examples
    Examples_FOL
    Example_Metric

session "HOL-SET_Protocol" (timing) in SET_Protocol = "HOL-Library" +
  description "
    Verification of the SET Protocol.
  "
  theories
    SET_Protocol
  document_files "root.tex"

session "HOL-Matrix_LP" in Matrix_LP = "HOL-Library" +
  description "
    Two-dimensional matrices and linear programming.
  "
  directories "Compute_Oracle"
  theories Cplex
  document_files "root.tex"

session "HOL-TLA" in TLA = HOL +
  description "
    Lamport's Temporal Logic of Actions.
  "
  theories TLA

session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
  theories Inc

session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
  theories DBuffer

session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
  theories MemoryImplementation

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

    TPTP-related extensions.
  "
  theories
    ATP_Theory_Export
    MaSh_Eval
    TPTP_Interpret
    THF_Arith
    TPTP_Proof_Reconstruction
  theories
    ATP_Problem_Import

session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
  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-Library" +
  theories
    Nominal

session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" +
  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.
  "
  theories
    Cardinals
    Bounded_Set
  document_files
    "intro.tex"
    "root.tex"
    "root.bib"

session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" +
  description "
    (Co)datatype Examples.
  "
  directories "Derivation_Trees"
  theories
    Compat
    Lambda_Term
    Process
    TreeFsetI
    "Derivation_Trees/Gram_Lang"
    "Derivation_Trees/Parallel_Composition"
    Koenig
    Lift_BNF
    Milner_Tofte
    Stream_Processor
    Misc_Codatatype
    Misc_Datatype
    Misc_Primcorec
    Misc_Primrec

session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" +
  description "
    Corecursion Examples.
  "
  directories "Tests"
  theories
    LFilter
    Paper_Examples
    Stream_Processor
    "Tests/Simple_Nesting"
    "Tests/Iterate_GPV"
  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 +
  sessions
    "HOL-Library"
  theories
    Word
    More_Word
    Word_Examples
  document_files "root.bib" "root.tex"

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

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

session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
  theories
    NSPrimes

session "HOL-Mirabelle" in Mirabelle = HOL +
  theories Mirabelle_Test

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

session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" +
  options [quick_and_dirty]
  theories
    Boogie
    SMT_Examples
    SMT_Word_Examples
    SMT_Tests

session "HOL-SPARK" in "SPARK" = "HOL-Word" +
  theories
    SPARK

session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
  directories "Gcd" "Liseq" "RIPEMD-160" "Sqrt"
  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"
  export_files (in ".") "*:**.prv"

session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
  options [show_question_marks = false]
  sessions
    "HOL-SPARK-Examples"
  theories
    Example_Verification
    VC_Principles
    Reference
    Complex_Types
  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-Library" +
  theories MutabelleExtra

session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = "HOL-Library" +
  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-Algebra" +
  description "
    Author:     Cezary Kaliszyk and Christian Urban
  "
  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-Library" +
  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 "HOL-Types_To_Sets" in Types_To_Sets = HOL +
  description "
    Experimental extension of Higher-Order Logic to allow translation of types to sets.
  "
  directories "Examples"
  theories
    Types_To_Sets
    "Examples/Prerequisites"
    "Examples/Finite"
    "Examples/T2_Spaces"
    "Examples/Unoverload_Def"
    "Examples/Linear_Algebra_On"

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

    HOLCF -- a semantic extension of HOL by the LCF logic.
  "
  sessions
    "HOL-Library"
  theories
    HOLCF (global)
  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 +
  theories
    HOLCF_Library
    HOL_Cpo

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.
  "
  sessions
    "HOL-IMP"
  theories
    HoareEx
  document_files
    "isaverbatimwrite.sty"
    "root.tex"
    "root.bib"

session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" +
  description "
    Miscellaneous examples for HOLCF.
  "
  theories
    Dnat
    Dagstuhl
    Focus_ex
    Fix2
    Hoare
    Concurrency_Monad
    Loop
    Powerdomain_ex
    Domain_Proofs
    Letrec
    Pattern_Match

session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" +
  description \<open>
    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
  \<close>
  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.
  "
  theories Abstraction

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

    The Alternating Bit Protocol performed in I/O-Automata.
  "
  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.
  "
  theories Correctness

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

    Memory storage case study.
  "
  theories Correctness

session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
  description "
    Author:     Olaf Mueller
  "
  theories
    TrivEx
    TrivEx2