wenzelm@48349: session HOL! (1) in "." = Pure +
wenzelm@48338:   description {* Classical Higher-order Logic *}
wenzelm@48338:   options [document_graph]
wenzelm@48338:   theories Complex_Main
wenzelm@48481:   files "document/root.bib" "document/root.tex"
wenzelm@48338: 
wenzelm@48338: session "HOL-Base"! in "." = Pure +
wenzelm@48338:   description {* Raw HOL base, with minimal tools *}
wenzelm@48470:   options [document = false]
wenzelm@48338:   theories HOL
wenzelm@48338: 
wenzelm@48338: session "HOL-Plain"! in "." = Pure +
wenzelm@48338:   description {* HOL side-entry after bootstrap of many tools and packages *}
wenzelm@48470:   options [document = false]
wenzelm@48338:   theories Plain
wenzelm@48338: 
wenzelm@48338: session "HOL-Main"! in "." = Pure +
wenzelm@48338:   description {* HOL side-entry for Main only, without Complex_Main *}
wenzelm@48470:   options [document = false]
wenzelm@48338:   theories Main
wenzelm@48338: 
wenzelm@48349: session "HOL-Proofs"! (2) in "." = Pure +
wenzelm@48338:   description {* HOL-Main with proof terms *}
wenzelm@48470:   options [document = false, proofs = 2, parallel_proofs = 0]
wenzelm@48338:   theories Main
wenzelm@48338: 
wenzelm@48481: session Library = HOL +
wenzelm@48481:   description {* Classical Higher-order Logic -- batteries included *}
wenzelm@48481:   theories
wenzelm@48481:     Library
wenzelm@48481:     List_Prefix
wenzelm@48481:     List_lexord
wenzelm@48481:     Sublist_Order
wenzelm@48481:     Product_Lattice
wenzelm@48481:     Code_Char_chr
wenzelm@48481:     Code_Char_ord
wenzelm@48481:     Code_Integer
wenzelm@48481:     Efficient_Nat
wenzelm@48481:     (*"Code_Prolog" FIXME*)
wenzelm@48481:     Code_Real_Approx_By_Float
wenzelm@48481:     Target_Numeral
wenzelm@48481:   files "document/root.bib" "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session Hahn_Banach = HOL +
wenzelm@48481:   description {*
wenzelm@48481:     Author:     Gertrud Bauer, TU Munich
wenzelm@48481: 
wenzelm@48481:     The Hahn-Banach theorem for real vector spaces.
wenzelm@48481:   *}
wenzelm@48481:   options [document_graph]
wenzelm@48481:   theories Hahn_Banach
wenzelm@48481:   files "document/root.bib" "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session Induct = HOL +
wenzelm@48481:   theories [quick_and_dirty]
wenzelm@48481:     Common_Patterns
wenzelm@48481:   theories
wenzelm@48481:     QuoDataType
wenzelm@48481:     QuoNestedDataType
wenzelm@48481:     Term
wenzelm@48481:     SList
wenzelm@48481:     ABexp
wenzelm@48481:     Tree
wenzelm@48481:     Ordinals
wenzelm@48481:     Sigma_Algebra
wenzelm@48481:     Comb
wenzelm@48481:     PropLog
wenzelm@48481:     Com
wenzelm@48481:   files "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session IMP = HOL +
wenzelm@48481:   options [document_graph]
wenzelm@48481:   theories [document = false]
wenzelm@48481:     "~~/src/HOL/ex/Interpretation_with_Defs"
wenzelm@48481:     "~~/src/HOL/Library/While_Combinator"
wenzelm@48481:     "~~/src/HOL/Library/Char_ord"
wenzelm@48481:     "~~/src/HOL/Library/List_lexord"
wenzelm@48481:   theories
wenzelm@48481:     BExp
wenzelm@48481:     ASM
wenzelm@48481:     Small_Step
wenzelm@48481:     Denotation
wenzelm@48481:     Comp_Rev
wenzelm@48481:     Poly_Types
wenzelm@48481:     Sec_Typing
wenzelm@48481:     Sec_TypingT
wenzelm@48481:     Def_Ass_Sound_Big
wenzelm@48481:     Def_Ass_Sound_Small
wenzelm@48481:     Live
wenzelm@48481:     Live_True
wenzelm@48481:     Hoare_Examples
wenzelm@48481:     VC
wenzelm@48481:     HoareT
wenzelm@48481:     Collecting1
wenzelm@48481:     Collecting_list
wenzelm@48481:     Abs_Int_Tests
wenzelm@48481:     Abs_Int1_parity
wenzelm@48481:     Abs_Int1_const
wenzelm@48481:     Abs_Int3
wenzelm@48481:     "Abs_Int_ITP/Abs_Int1_parity_ITP"
wenzelm@48481:     "Abs_Int_ITP/Abs_Int1_const_ITP"
wenzelm@48481:     "Abs_Int_ITP/Abs_Int3_ITP"
wenzelm@48481:     "Abs_Int_Den/Abs_Int_den2"
wenzelm@48481:     Procs_Dyn_Vars_Dyn
wenzelm@48481:     Procs_Stat_Vars_Dyn
wenzelm@48481:     Procs_Stat_Vars_Stat
wenzelm@48481:     C_like
wenzelm@48481:     OO
wenzelm@48481:     Fold
wenzelm@48481:   files "document/root.bib" "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session IMPP = HOL +
wenzelm@48481:   description {*
wenzelm@48481:     Author:     David von Oheimb
wenzelm@48481:     Copyright   1999 TUM
wenzelm@48481:   *}
wenzelm@48481:   theories EvenOdd
wenzelm@48481: 
wenzelm@48481: session Import = HOL +
wenzelm@48481:   options [document_graph]
wenzelm@48481:   theories HOL_Light_Maps
wenzelm@48481:   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
wenzelm@48481: 
wenzelm@48481: session Number_Theory = HOL +
wenzelm@48481:   theories Number_Theory
wenzelm@48481: 
wenzelm@48481: session Old_Number_Theory = HOL +
wenzelm@48481:   options [document_graph]
wenzelm@48481:   theories [document = false]
wenzelm@48481:     "~~/src/HOL/Library/Infinite_Set"
wenzelm@48481:     "~~/src/HOL/Library/Permutation"
wenzelm@48481:   theories
wenzelm@48481:     Fib
wenzelm@48481:     Factorization
wenzelm@48481:     Chinese
wenzelm@48481:     WilsonRuss
wenzelm@48481:     WilsonBij
wenzelm@48481:     Quadratic_Reciprocity
wenzelm@48481:     Primes
wenzelm@48481:     Pocklington
wenzelm@48481:   files "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session Hoare = HOL +
wenzelm@48481:   theories Hoare
wenzelm@48481:   files "document/root.bib" "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session Hoare_Parallel = HOL +
wenzelm@48481:   options [document_graph]
wenzelm@48481:   theories Hoare_Parallel
wenzelm@48481:   files "document/root.bib" "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session Codegenerator_Test = "HOL-Library" +
wenzelm@48481:   options [document = false, document_graph = false, browser_info = false]
wenzelm@48481:   theories Generate Generate_Pretty
wenzelm@48481: 
wenzelm@48481: session Metis_Examples = HOL +
wenzelm@48481:   description {*
wenzelm@48481:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@48481:     Author:     Jasmin Blanchette, TU Muenchen
wenzelm@48481: 
wenzelm@48481:     Testing Metis and Sledgehammer.
wenzelm@48481:   *}
wenzelm@48481:   theories
wenzelm@48481:     Abstraction
wenzelm@48481:     Big_O
wenzelm@48481:     Binary_Tree
wenzelm@48481:     Clausification
wenzelm@48481:     Message
wenzelm@48481:     Proxies
wenzelm@48481:     Tarski
wenzelm@48481:     Trans_Closure
wenzelm@48481:     Sets
wenzelm@48481: 
wenzelm@48481: session Nitpick_Examples = HOL +
wenzelm@48481:   description {*
wenzelm@48481:     Author:     Jasmin Blanchette, TU Muenchen
wenzelm@48481:     Copyright   2009
wenzelm@48481:   *}
wenzelm@48481:   theories [quick_and_dirty] Nitpick_Examples
wenzelm@48481: 
wenzelm@48481: session Algebra = HOL +
wenzelm@48481:   description {*
wenzelm@48481:     Author: Clemens Ballarin, started 24 September 1999
wenzelm@48481: 
wenzelm@48481:     The Isabelle Algebraic Library.
wenzelm@48481:   *}
wenzelm@48481:   options [document_graph]
wenzelm@48481:   theories [document = false]
wenzelm@48481:     (* Preliminaries from set and number theory *)
wenzelm@48481:     "~~/src/HOL/Library/FuncSet"
wenzelm@48481:     "~~/src/HOL/Old_Number_Theory/Primes"
wenzelm@48481:     "~~/src/HOL/Library/Binomial"
wenzelm@48481:     "~~/src/HOL/Library/Permutation"
wenzelm@48481:   theories
wenzelm@48481:     (*** New development, based on explicit structures ***)
wenzelm@48481:     (* Groups *)
wenzelm@48481:     FiniteProduct        (* Product operator for commutative groups *)
wenzelm@48481:     Sylow                (* Sylow's theorem *)
wenzelm@48481:     Bij                  (* Automorphism Groups *)
wenzelm@48481: 
wenzelm@48481:     (* Rings *)
wenzelm@48481:     Divisibility         (* Rings *)
wenzelm@48481:     IntRing              (* Ideals and residue classes *)
wenzelm@48481:     UnivPoly             (* Polynomials *)
wenzelm@48481:   theories [document = false]
wenzelm@48481:     (*** Old development, based on axiomatic type classes ***)
wenzelm@48481:     "abstract/Abstract"  (*The ring theory*)
wenzelm@48481:     "poly/Polynomial"    (*The full theory*)
wenzelm@48481:   files "document/root.bib" "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session Auth = HOL +
wenzelm@48481:   options [document_graph]
wenzelm@48481:   theories
wenzelm@48481:     Auth_Shared
wenzelm@48481:     Auth_Public
wenzelm@48481:     "Smartcard/Auth_Smartcard"
wenzelm@48481:     "Guard/Auth_Guard_Shared"
wenzelm@48481:     "Guard/Auth_Guard_Public"
wenzelm@48481:   files "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session UNITY = HOL +
wenzelm@48481:   description {*
wenzelm@48481:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@48481:     Copyright   1998  University of Cambridge
wenzelm@48481: 
wenzelm@48481:     Verifying security protocols using UNITY.
wenzelm@48481:   *}
wenzelm@48481:   options [document_graph]
wenzelm@48481:   theories [document = false] "../Auth/Public"
wenzelm@48481:   theories
wenzelm@48481:     (*Basic meta-theory*)
wenzelm@48481:     "UNITY_Main"
wenzelm@48481: 
wenzelm@48481:     (*Simple examples: no composition*)
wenzelm@48481:     "Simple/Deadlock"
wenzelm@48481:     "Simple/Common"
wenzelm@48481:     "Simple/Network"
wenzelm@48481:     "Simple/Token"
wenzelm@48481:     "Simple/Channel"
wenzelm@48481:     "Simple/Lift"
wenzelm@48481:     "Simple/Mutex"
wenzelm@48481:     "Simple/Reach"
wenzelm@48481:     "Simple/Reachability"
wenzelm@48481: 
wenzelm@48481:     (*Verifying security protocols using UNITY*)
wenzelm@48481:     "Simple/NSP_Bad"
wenzelm@48481: 
wenzelm@48481:     (*Example of composition*)
wenzelm@48481:     "Comp/Handshake"
wenzelm@48481: 
wenzelm@48481:     (*Universal properties examples*)
wenzelm@48481:     "Comp/Counter"
wenzelm@48481:     "Comp/Counterc"
wenzelm@48481:     "Comp/Priority"
wenzelm@48481: 
wenzelm@48481:     "Comp/TimerArray"
wenzelm@48481:     "Comp/Progress"
wenzelm@48481: 
wenzelm@48481:     "Comp/Alloc"
wenzelm@48481:     "Comp/AllocImpl"
wenzelm@48481:     "Comp/Client"
wenzelm@48481: 
wenzelm@48481:     (*obsolete*)
wenzelm@48481:     "ELT"
wenzelm@48481:   files "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session Unix = HOL +
wenzelm@48481:   options [print_mode = "no_brackets,no_type_brackets"]
wenzelm@48481:   theories Unix
wenzelm@48481:   files "document/root.bib" "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session ZF = HOL +
wenzelm@48481:   description {* *}
wenzelm@48481:   theories MainZF Games
wenzelm@48481:   files "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session Imperative_HOL = HOL +
wenzelm@48481:   description {* *}
wenzelm@48481:   options [document_graph, print_mode = "iff,no_brackets"]
wenzelm@48481:   theories [document = false]
wenzelm@48481:     "~~/src/HOL/Library/Countable"
wenzelm@48481:     "~~/src/HOL/Library/Monad_Syntax"
wenzelm@48481:     "~~/src/HOL/Library/Code_Natural"
wenzelm@48481:     "~~/src/HOL/Library/LaTeXsugar"
wenzelm@48481:   theories Imperative_HOL_ex
wenzelm@48481:   files "document/root.bib" "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session Decision_Procs = HOL +
wenzelm@48481:   theories Decision_Procs
wenzelm@48481: 
wenzelm@48481: session ex in "Proofs/ex" = "HOL-Proofs" +
wenzelm@48481:   options [proofs = 2, parallel_proofs = 0]
wenzelm@48481:   theories Hilbert_Classical
wenzelm@48481: 
wenzelm@48481: session Extraction in "Proofs/Extraction" = "HOL-Proofs" +
wenzelm@48481:   description {* Examples for program extraction in Higher-Order Logic *}
wenzelm@48481:   options [proofs = 2, parallel_proofs = 0]
wenzelm@48481:   theories [document = false]
wenzelm@48481:     "~~/src/HOL/Library/Efficient_Nat"
wenzelm@48481:     "~~/src/HOL/Library/Monad_Syntax"
wenzelm@48481:     "~~/src/HOL/Number_Theory/Primes"
wenzelm@48481:     "~~/src/HOL/Number_Theory/UniqueFactorization"
wenzelm@48481:     "~~/src/HOL/Library/State_Monad"
wenzelm@48481:   theories
wenzelm@48481:     Greatest_Common_Divisor
wenzelm@48481:     Warshall
wenzelm@48481:     Higman_Extraction
wenzelm@48481:     Pigeonhole
wenzelm@48481:     Euclid
wenzelm@48481:   files "document/root.bib" "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session Lambda in "Proofs/Lambda" = "HOL-Proofs" +
wenzelm@48481:   options [document_graph, print_mode = "no_brackets", proofs = 2, parallel_proofs = 0]
wenzelm@48481:   theories [document = false]
wenzelm@48481:     "~~/src/HOL/Library/Code_Integer"
wenzelm@48481:   theories
wenzelm@48481:     Eta
wenzelm@48481:     StrongNorm
wenzelm@48481:     Standardization
wenzelm@48481:     WeakNorm
wenzelm@48481:   files "document/root.bib" "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session Prolog = HOL +
wenzelm@48481:   description {*
wenzelm@48481:     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
wenzelm@48481:   *}
wenzelm@48481:   theories Test Type
wenzelm@48481: 
wenzelm@48481: session MicroJava = HOL +
wenzelm@48481:   options [document_graph]
wenzelm@48481:   theories [document = false] "~~/src/HOL/Library/While_Combinator"
wenzelm@48481:   theories MicroJava
wenzelm@48481:   files
wenzelm@48481:     "document/introduction.tex"
wenzelm@48481:     "document/root.bib"
wenzelm@48481:     "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session NanoJava = HOL +
wenzelm@48481:   options [document_graph]
wenzelm@48481:   theories Example
wenzelm@48481:   files "document/root.bib" "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session Bali = HOL +
wenzelm@48481:   options [document_graph]
wenzelm@48481:   theories
wenzelm@48481:     AxExample
wenzelm@48481:     AxSound
wenzelm@48481:     AxCompl
wenzelm@48481:     Trans
wenzelm@48481:   files "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session IOA = HOL +
wenzelm@48481:   description {*
wenzelm@48481:     Author:     Tobias Nipkow & Konrad Slind
wenzelm@48481:     Copyright   1994  TU Muenchen
wenzelm@48481: 
wenzelm@48481:     The meta theory of I/O-Automata.
wenzelm@48481: 
wenzelm@48481:     @inproceedings{Nipkow-Slind-IOA,
wenzelm@48481:     author={Tobias Nipkow and Konrad Slind},
wenzelm@48481:     title={{I/O} Automata in {Isabelle/HOL}},
wenzelm@48481:     booktitle={Proc.\ TYPES Workshop 1994},
wenzelm@48481:     publisher=Springer,
wenzelm@48481:     series=LNCS,
wenzelm@48481:     note={To appear}}
wenzelm@48481:     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
wenzelm@48481: 
wenzelm@48481:     and
wenzelm@48481: 
wenzelm@48481:     @inproceedings{Mueller-Nipkow,
wenzelm@48481:     author={Olaf M\"uller and Tobias Nipkow},
wenzelm@48481:     title={Combining Model Checking and Deduction for {I/O}-Automata},
wenzelm@48481:     booktitle={Proc.\ TACAS Workshop},
wenzelm@48481:     organization={Aarhus University, BRICS report},
wenzelm@48481:     year=1995}
wenzelm@48481:     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
wenzelm@48481:   *}
wenzelm@48481:   theories Solve
wenzelm@48481: 
wenzelm@48481: session Lattice = HOL +
wenzelm@48481:   description {*
wenzelm@48481:     Author:     Markus Wenzel, TU Muenchen
wenzelm@48481: 
wenzelm@48481:     Basic theory of lattices and orders.
wenzelm@48481:   *}
wenzelm@48481:   theories CompleteLattice
wenzelm@48481:   files "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session ex = HOL +
wenzelm@48481:   description {* Miscellaneous examples for Higher-Order Logic. *}
wenzelm@48481:   theories [document = false]
wenzelm@48481:     "~~/src/HOL/Library/State_Monad"
wenzelm@48481:     Code_Nat_examples
wenzelm@48481:     "~~/src/HOL/Library/FuncSet"
wenzelm@48481:     Eval_Examples
wenzelm@48481:     Normalization_by_Evaluation
wenzelm@48481:     Hebrew
wenzelm@48481:     Chinese
wenzelm@48481:     Serbian
wenzelm@48481:     "~~/src/HOL/Library/FinFun_Syntax"
wenzelm@48481:   theories
wenzelm@48481:     Iff_Oracle
wenzelm@48481:     Coercion_Examples
wenzelm@48481:     Numeral_Representation
wenzelm@48481:     Higher_Order_Logic
wenzelm@48481:     Abstract_NAT
wenzelm@48481:     Guess
wenzelm@48481:     Binary
wenzelm@48481:     Fundefs
wenzelm@48481:     Induction_Schema
wenzelm@48481:     LocaleTest2
wenzelm@48481:     Records
wenzelm@48481:     While_Combinator_Example
wenzelm@48481:     MonoidGroup
wenzelm@48481:     BinEx
wenzelm@48481:     Hex_Bin_Examples
wenzelm@48481:     Antiquote
wenzelm@48481:     Multiquote
wenzelm@48481:     PER
wenzelm@48481:     NatSum
wenzelm@48481:     ThreeDivides
wenzelm@48481:     Intuitionistic
wenzelm@48481:     CTL
wenzelm@48481:     Arith_Examples
wenzelm@48481:     BT
wenzelm@48481:     Tree23
wenzelm@48481:     MergeSort
wenzelm@48481:     Lagrange
wenzelm@48481:     Groebner_Examples
wenzelm@48481:     MT
wenzelm@48481:     Unification
wenzelm@48481:     Primrec
wenzelm@48481:     Tarski
wenzelm@48481:     Classical
wenzelm@48481:     Set_Theory
wenzelm@48481:     Meson_Test
wenzelm@48481:     Termination
wenzelm@48481:     Coherent
wenzelm@48481:     PresburgerEx
wenzelm@48481:     ReflectionEx
wenzelm@48481:     Sqrt
wenzelm@48481:     Sqrt_Script
wenzelm@48481:     Transfer_Ex
wenzelm@48481:     Transfer_Int_Nat
wenzelm@48481:     HarmonicSeries
wenzelm@48481:     Refute_Examples
wenzelm@48481:     Landau
wenzelm@48481:     Execute_Choice
wenzelm@48481:     Summation
wenzelm@48481:     Gauge_Integration
wenzelm@48481:     Dedekind_Real
wenzelm@48481:     Quicksort
wenzelm@48481:     Birthday_Paradox
wenzelm@48481:     List_to_Set_Comprehension_Examples
wenzelm@48481:     Seq
wenzelm@48481:     Simproc_Tests
wenzelm@48481:     Executable_Relation
wenzelm@48481:     FinFunPred
wenzelm@48481:     Set_Comprehension_Pointfree_Tests
wenzelm@48481:     Parallel_Example
wenzelm@48481:   theories SVC_Oracle
wenzelm@48481:   theories [condition = SVC_HOME] svc_test
wenzelm@48481:   theories [condition = ZCHAFF_HOME]
wenzelm@48481:     (*requires zChaff (or some other reasonably fast SAT solver)*)
wenzelm@48481:     Sudoku
wenzelm@48481: (* FIXME
wenzelm@48481: (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
wenzelm@48481: (*global side-effects ahead!*)
wenzelm@48481: try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)
wenzelm@48481: *)
wenzelm@48481:   files "document/root.bib" "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session Isar_Examples = HOL +
wenzelm@48481:   description {* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *}
wenzelm@48481:   theories [document = false]
wenzelm@48481:     "~~/src/HOL/Library/Lattice_Syntax"
wenzelm@48481:     "../Number_Theory/Primes"
wenzelm@48481:   theories
wenzelm@48481:     Basic_Logic
wenzelm@48481:     Cantor
wenzelm@48481:     Drinker
wenzelm@48481:     Expr_Compiler
wenzelm@48481:     Fibonacci
wenzelm@48481:     Group
wenzelm@48481:     Group_Context
wenzelm@48481:     Group_Notepad
wenzelm@48481:     Hoare_Ex
wenzelm@48481:     Knaster_Tarski
wenzelm@48481:     Mutilated_Checkerboard
wenzelm@48481:     Nested_Datatype
wenzelm@48481:     Peirce
wenzelm@48481:     Puzzle
wenzelm@48481:     Summation
wenzelm@48481:   files
wenzelm@48481:     "document/root.bib"
wenzelm@48481:     "document/root.tex"
wenzelm@48481:     "document/style.tex"
wenzelm@48481: 
wenzelm@48481: session SET_Protocol = HOL +
wenzelm@48481:   options [document_graph]
wenzelm@48481:   theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
wenzelm@48481:   theories SET_Protocol
wenzelm@48481:   files "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session Matrix_LP = HOL +
wenzelm@48481:   options [document_graph]
wenzelm@48481:   theories Cplex
wenzelm@48481:   files "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session TLA! = HOL +
wenzelm@48481:   description {* The Temporal Logic of Actions *}
wenzelm@48481:   theories TLA
wenzelm@48481: 
wenzelm@48481: session Inc in "TLA/Inc" = TLA +
wenzelm@48481:   theories Inc
wenzelm@48481: 
wenzelm@48481: session Buffer in "TLA/Buffer" = TLA +
wenzelm@48481:   theories DBuffer
wenzelm@48481: 
wenzelm@48481: session Memory in "TLA/Memory" = TLA +
wenzelm@48481:   theories MemoryImplementation
wenzelm@48481: 
wenzelm@48481: session TPTP = HOL +
wenzelm@48481:   description {*
wenzelm@48481:     Author:     Jasmin Blanchette, TU Muenchen
wenzelm@48481:     Author:     Nik Sultana, University of Cambridge
wenzelm@48481:     Copyright   2011
wenzelm@48481: 
wenzelm@48481:     TPTP-related extensions.
wenzelm@48481:   *}
wenzelm@48481:   theories
wenzelm@48481:     ATP_Theory_Export
wenzelm@48481:     MaSh_Eval
wenzelm@48481:     MaSh_Export
wenzelm@48481:     TPTP_Interpret
wenzelm@48481:     THF_Arith
wenzelm@48481:   theories [proofs = 0]  (* FIXME !? *)
wenzelm@48481:     ATP_Problem_Import
wenzelm@48481: 
wenzelm@48481: session Multivariate_Analysis = HOL +
wenzelm@48481:   options [document_graph]
wenzelm@48481:   theories
wenzelm@48481:     Multivariate_Analysis
wenzelm@48481:     Determinants
wenzelm@48481:   files
wenzelm@48481:     "Integration.certs"
wenzelm@48481:     "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session "HOL-Probability"! in "Probability" = "HOL-Multivariate_Analysis" +
wenzelm@48481:   options [document_graph]
wenzelm@48481:   theories [document = false]
wenzelm@48481:     "~~/src/HOL/Library/Countable"
wenzelm@48481:     "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
wenzelm@48481:     "~~/src/HOL/Library/Permutation"
wenzelm@48481:   theories
wenzelm@48481:     Probability
wenzelm@48481:     "ex/Dining_Cryptographers"
wenzelm@48481:     "ex/Koepf_Duermuth_Countermeasure"
wenzelm@48481:   files "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session Nominal = HOL +
wenzelm@48481:   theories Nominal
wenzelm@48481: 
wenzelm@48481: session Examples in "Nominal/Examples" = "HOL-Nominal" +
wenzelm@48481:   theories Nominal_Examples
wenzelm@48481:   theories [quick_and_dirty] VC_Condition
wenzelm@48481: 
wenzelm@48481: session Word = HOL +
wenzelm@48481:   options [document_graph]
wenzelm@48481:   theories Word
wenzelm@48481:   files "document/root.bib" "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session Examples in "Word/Examples" = "HOL-Word" +
wenzelm@48481:   theories WordExamples
wenzelm@48481: 
wenzelm@48481: session Statespace = HOL +
wenzelm@48481:   theories StateSpaceEx
wenzelm@48481:   files "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session NSA = HOL +
wenzelm@48481:   options [document_graph]
wenzelm@48481:   theories Hypercomplex
wenzelm@48481:   files "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session Examples in "NSA/Examples" = "HOL-NSA" +
wenzelm@48481:   theories NSPrimes
wenzelm@48481: 
wenzelm@48481: session Mirabelle = HOL +
wenzelm@48481:   theories Mirabelle_Test
wenzelm@48481: (* FIXME
wenzelm@48481: 	@cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case
wenzelm@48481: *)
wenzelm@48481: 
wenzelm@48481: session SMT_Examples = "HOL-Word" +
wenzelm@48481:   options [quick_and_dirty]
wenzelm@48481:   theories
wenzelm@48481:     SMT_Tests
wenzelm@48481:     SMT_Examples
wenzelm@48481:     SMT_Word_Examples
wenzelm@48481:   files
wenzelm@48481:     "SMT_Examples.certs"
wenzelm@48481:     "SMT_Tests.certs"
wenzelm@48481: 
wenzelm@48481: session "HOL-Boogie"! in "Boogie" = "HOL-Word" +
wenzelm@48481:   theories Boogie
wenzelm@48481:   (* FIXME files!?! *)
wenzelm@48481: 
wenzelm@48481: session Examples in "Boogie/Examples" = "HOL-Boogie" +
wenzelm@48481:   theories
wenzelm@48481:     Boogie_Max_Stepwise
wenzelm@48481:     Boogie_Max
wenzelm@48481:     Boogie_Dijkstra
wenzelm@48481:     VCC_Max
wenzelm@48481:   files
wenzelm@48481:     "Boogie_Dijkstra.certs"
wenzelm@48481:     "Boogie_Max.certs"
wenzelm@48481:     "VCC_Max.certs"
wenzelm@48481: 
wenzelm@48481: session "HOL-SPARK"! in "SPARK" = "HOL-Word" +
wenzelm@48481:   theories SPARK
wenzelm@48481: 
wenzelm@48481: session Examples in "SPARK/Examples" = "HOL-SPARK" +
wenzelm@48481:   theories
wenzelm@48481:     "Gcd/Greatest_Common_Divisor"
wenzelm@48481: 
wenzelm@48481:     "Liseq/Longest_Increasing_Subsequence"
wenzelm@48481: 
wenzelm@48481:     "RIPEMD-160/F"
wenzelm@48481:     "RIPEMD-160/Hash"
wenzelm@48481:     "RIPEMD-160/K_L"
wenzelm@48481:     "RIPEMD-160/K_R"
wenzelm@48481:     "RIPEMD-160/R_L"
wenzelm@48481:     "RIPEMD-160/Round"
wenzelm@48481:     "RIPEMD-160/R_R"
wenzelm@48481:     "RIPEMD-160/S_L"
wenzelm@48481:     "RIPEMD-160/S_R"
wenzelm@48481: 
wenzelm@48481:     "Sqrt/Sqrt"
wenzelm@48481:   files
wenzelm@48481:     "Gcd/greatest_common_divisor/g_c_d.fdl"
wenzelm@48481:     "Gcd/greatest_common_divisor/g_c_d.rls"
wenzelm@48481:     "Gcd/greatest_common_divisor/g_c_d.siv"
wenzelm@48481:     "Liseq/liseq/liseq_length.fdl"
wenzelm@48481:     "Liseq/liseq/liseq_length.rls"
wenzelm@48481:     "Liseq/liseq/liseq_length.siv"
wenzelm@48481:     "RIPEMD-160/rmd/f.fdl"
wenzelm@48481:     "RIPEMD-160/rmd/f.rls"
wenzelm@48481:     "RIPEMD-160/rmd/f.siv"
wenzelm@48481:     "RIPEMD-160/rmd/hash.fdl"
wenzelm@48481:     "RIPEMD-160/rmd/hash.rls"
wenzelm@48481:     "RIPEMD-160/rmd/hash.siv"
wenzelm@48481:     "RIPEMD-160/rmd/k_l.fdl"
wenzelm@48481:     "RIPEMD-160/rmd/k_l.rls"
wenzelm@48481:     "RIPEMD-160/rmd/k_l.siv"
wenzelm@48481:     "RIPEMD-160/rmd/k_r.fdl"
wenzelm@48481:     "RIPEMD-160/rmd/k_r.rls"
wenzelm@48481:     "RIPEMD-160/rmd/k_r.siv"
wenzelm@48481:     "RIPEMD-160/rmd/r_l.fdl"
wenzelm@48481:     "RIPEMD-160/rmd/r_l.rls"
wenzelm@48481:     "RIPEMD-160/rmd/r_l.siv"
wenzelm@48481:     "RIPEMD-160/rmd/round.fdl"
wenzelm@48481:     "RIPEMD-160/rmd/round.rls"
wenzelm@48481:     "RIPEMD-160/rmd/round.siv"
wenzelm@48481:     "RIPEMD-160/rmd/r_r.fdl"
wenzelm@48481:     "RIPEMD-160/rmd/r_r.rls"
wenzelm@48481:     "RIPEMD-160/rmd/r_r.siv"
wenzelm@48481:     "RIPEMD-160/rmd/s_l.fdl"
wenzelm@48481:     "RIPEMD-160/rmd/s_l.rls"
wenzelm@48481:     "RIPEMD-160/rmd/s_l.siv"
wenzelm@48481:     "RIPEMD-160/rmd/s_r.fdl"
wenzelm@48481:     "RIPEMD-160/rmd/s_r.rls"
wenzelm@48481:     "RIPEMD-160/rmd/s_r.siv"
wenzelm@48481: 
wenzelm@48481: session Manual in "SPARK/Manual" = "HOL-SPARK" +
wenzelm@48481:   (* FIXME Printer.show_question_marks_default := false; *)
wenzelm@48481:   theories
wenzelm@48481:     Example_Verification
wenzelm@48481:     VC_Principles
wenzelm@48481:     Reference
wenzelm@48481:     Complex_Types
wenzelm@48481:   files
wenzelm@48481:     "complex_types_app/initialize.fdl"
wenzelm@48481:     "complex_types_app/initialize.rls"
wenzelm@48481:     "complex_types_app/initialize.siv"
wenzelm@48481:     "document/complex_types.ads"
wenzelm@48481:     "document/complex_types_app.adb"
wenzelm@48481:     "document/complex_types_app.ads"
wenzelm@48481:     "document/Gcd.adb"
wenzelm@48481:     "document/Gcd.ads"
wenzelm@48481:     "document/intro.tex"
wenzelm@48481:     "document/loop_invariant.adb"
wenzelm@48481:     "document/loop_invariant.ads"
wenzelm@48481:     "document/root.bib"
wenzelm@48481:     "document/root.tex"
wenzelm@48481:     "document/Simple_Gcd.adb"
wenzelm@48481:     "document/Simple_Gcd.ads"
wenzelm@48481:     "loop_invariant/proc1.fdl"
wenzelm@48481:     "loop_invariant/proc1.rls"
wenzelm@48481:     "loop_invariant/proc1.siv"
wenzelm@48481:     "loop_invariant/proc2.fdl"
wenzelm@48481:     "loop_invariant/proc2.rls"
wenzelm@48481:     "loop_invariant/proc2.siv"
wenzelm@48481:     "simple_greatest_common_divisor/g_c_d.fdl"
wenzelm@48481:     "simple_greatest_common_divisor/g_c_d.rls"
wenzelm@48481:     "simple_greatest_common_divisor/g_c_d.siv"
wenzelm@48481: 
wenzelm@48481: session Mutabelle = HOL +
wenzelm@48481:   theories MutabelleExtra
wenzelm@48481: 
wenzelm@48481: session Quickcheck_Examples = HOL +
wenzelm@48481:   theories Quickcheck_Examples  (* FIXME *)
wenzelm@48481: 
wenzelm@48481: session Quotient_Examples = HOL +
wenzelm@48481:   description {*
wenzelm@48481:     Author:     Cezary Kaliszyk and Christian Urban
wenzelm@48481:   *}
wenzelm@48481:   theories
wenzelm@48481:     DList
wenzelm@48481:     FSet
wenzelm@48481:     Quotient_Int
wenzelm@48481:     Quotient_Message
wenzelm@48481:     Lift_FSet
wenzelm@48481:     Lift_Set
wenzelm@48481:     Lift_RBT
wenzelm@48481:     Lift_Fun
wenzelm@48481:     Quotient_Rat
wenzelm@48481:     Lift_DList
wenzelm@48481: 
wenzelm@48481: session Predicate_Compile_Examples = HOL +
wenzelm@48481:   theories  (* FIXME *)
wenzelm@48481:     Examples
wenzelm@48481:     Predicate_Compile_Tests
wenzelm@48481:     Specialisation_Examples
wenzelm@48481: 
wenzelm@48349: session HOLCF! (3) = HOL +
wenzelm@48338:   description {*
wenzelm@48338:     Author:     Franz Regensburger
wenzelm@48338:     Author:     Brian Huffman
wenzelm@48338: 
wenzelm@48338:     HOLCF -- a semantic extension of HOL by the LCF logic.
wenzelm@48338:   *}
wenzelm@48338:   options [document_graph]
wenzelm@48470:   theories [document = false]
wenzelm@48338:     "~~/src/HOL/Library/Nat_Bijection"
wenzelm@48338:     "~~/src/HOL/Library/Countable"
wenzelm@48481:   theories
wenzelm@48481:     Plain_HOLCF
wenzelm@48481:     Fixrec
wenzelm@48481:     HOLCF
wenzelm@48481:   files "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session Tutorial in "HOLCF/Tutorial" = HOLCF +
wenzelm@48481:   theories
wenzelm@48481:     Domain_ex
wenzelm@48481:     Fixrec_ex
wenzelm@48481:     New_Domain
wenzelm@48481:   files "document/root.tex"
wenzelm@48481: 
wenzelm@48481: session Library in "HOLCF/Library" = HOLCF +
wenzelm@48481:   theories HOLCF_Library
wenzelm@48481: 
wenzelm@48481: session IMP in "HOLCF/IMP" = HOLCF +
wenzelm@48481:   theories HoareEx
wenzelm@48338:   files "document/root.tex"
wenzelm@48338: 
wenzelm@48481: session ex in "HOLCF/ex" = HOLCF +
wenzelm@48481:   description {* Misc HOLCF examples *}
wenzelm@48481:   theories
wenzelm@48481:     Dnat
wenzelm@48481:     Dagstuhl
wenzelm@48481:     Focus_ex
wenzelm@48481:     Fix2
wenzelm@48481:     Hoare
wenzelm@48481:     Concurrency_Monad
wenzelm@48481:     Loop
wenzelm@48481:     Powerdomain_ex
wenzelm@48481:     Domain_Proofs
wenzelm@48481:     Letrec
wenzelm@48481:     Pattern_Match
wenzelm@48481: 
wenzelm@48481: session FOCUS in "HOLCF/FOCUS" = HOLCF +
wenzelm@48481:   theories
wenzelm@48481:     Fstreams
wenzelm@48481:     FOCUS
wenzelm@48481:     Buffer_adm
wenzelm@48481: 
wenzelm@48481: session IOA! in "HOLCF/IOA" = HOLCF +
wenzelm@48481:   description {*
wenzelm@48481:     Author:     Olaf Mueller
wenzelm@48481: 
wenzelm@48481:     Formalization of a semantic model of I/O-Automata.
wenzelm@48481:   *}
wenzelm@48481:   theories "meta_theory/Abstraction"
wenzelm@48481: 
wenzelm@48481: session ABP in "HOLCF/IOA/ABP" = IOA +
wenzelm@48481:   description {*
wenzelm@48481:     Author:     Olaf Mueller
wenzelm@48481: 
wenzelm@48481:     The Alternating Bit Protocol performed in I/O-Automata.
wenzelm@48481:   *}
wenzelm@48481:   theories Correctness
wenzelm@48481: 
wenzelm@48481: session NTP in "HOLCF/IOA/NTP" = IOA +
wenzelm@48481:   description {*
wenzelm@48481:     Author:     Tobias Nipkow & Konrad Slind
wenzelm@48481: 
wenzelm@48481:     A network transmission protocol, performed in the
wenzelm@48481:     I/O automata formalization by Olaf Mueller.
wenzelm@48481:   *}
wenzelm@48481:   theories Correctness
wenzelm@48481: 
wenzelm@48481: session Storage in "HOLCF/IOA/Storage" = IOA +
wenzelm@48481:   description {*
wenzelm@48481:     Author:     Olaf Mueller
wenzelm@48481: 
wenzelm@48481:     Memory storage case study.
wenzelm@48481:   *}
wenzelm@48481:   theories Correctness
wenzelm@48481: 
wenzelm@48481: session ex in "HOLCF/IOA/ex" = IOA +
wenzelm@48481:   description {*
wenzelm@48481:     Author:     Olaf Mueller
wenzelm@48481:   *}
wenzelm@48481:   theories
wenzelm@48481:     TrivEx
wenzelm@48481:     TrivEx2
wenzelm@48481: 
wenzelm@48481: session Datatype_Benchmark = HOL +
wenzelm@48481:   description {* Some rather large datatype examples (from John Harrison). *}
wenzelm@48481:   theories [condition = ISABELLE_BENCHMARK]
wenzelm@48481:     (* FIXME Toplevel.timing := true; *)
wenzelm@48481:     Brackin
wenzelm@48481:     Instructions
wenzelm@48481:     SML
wenzelm@48481:     Verilog
wenzelm@48481: 
wenzelm@48481: session Record_Benchmark = HOL +
wenzelm@48481:   description {* Some benchmark on large record. *}
wenzelm@48481:   theories [condition = ISABELLE_BENCHMARK]
wenzelm@48481:     (* FIXME Toplevel.timing := true; *)
wenzelm@48481:     Record_Benchmark
wenzelm@48481: 
wenzelm@48481: