wenzelm@51397: chapter HOL wenzelm@51397: wenzelm@48738: session HOL (main) = Pure + wenzelm@51421: description {* wenzelm@51421: Classical Higher-order Logic. wenzelm@51421: *} wenzelm@48338: options [document_graph] wenzelm@48338: theories Complex_Main wenzelm@48901: files wenzelm@48901: "Tools/Quickcheck/Narrowing_Engine.hs" wenzelm@48901: "Tools/Quickcheck/PNF_Narrowing_Engine.hs" wenzelm@48901: "document/root.bib" wenzelm@48901: "document/root.tex" wenzelm@48338: wenzelm@48738: session "HOL-Proofs" = Pure + wenzelm@51421: description {* wenzelm@51421: HOL-Main with explicit proof terms. wenzelm@51421: *} wenzelm@52499: options [document = false] wenzelm@52488: theories Proofs (*sequential change of global flag!*) wenzelm@48338: theories Main wenzelm@48901: files wenzelm@48901: "Tools/Quickcheck/Narrowing_Engine.hs" wenzelm@48901: "Tools/Quickcheck/PNF_Narrowing_Engine.hs" wenzelm@48338: wenzelm@50844: session "HOL-Library" (main) in Library = HOL + wenzelm@51421: description {* wenzelm@51421: Classical Higher-order Logic -- batteries included. wenzelm@51421: *} wenzelm@48481: theories wenzelm@48481: Library haftmann@51161: (*conflicting type class instantiations*) wenzelm@48481: List_lexord wenzelm@48481: Sublist_Order haftmann@51115: Product_Lexorder haftmann@51115: Product_Order haftmann@51161: Finite_Lattice haftmann@51161: (*data refinements and dependent applications*) haftmann@51161: AList_Mapping haftmann@51161: Code_Binary_Nat haftmann@51161: Code_Char wenzelm@48721: (* Code_Prolog FIXME cf. 76965c356d2a *) wenzelm@48481: Code_Real_Approx_By_Float haftmann@50023: Code_Target_Numeral haftmann@51161: DAList haftmann@54429: DAList_Multiset haftmann@51161: RBT_Mapping haftmann@51161: RBT_Set haftmann@51161: (*legacy tools*) blanchet@49985: Refute haftmann@51161: Old_Recdef wenzelm@48932: theories [condition = ISABELLE_FULL_TEST] wenzelm@48932: Sum_of_Squares_Remote wenzelm@48481: files "document/root.bib" "document/root.tex" wenzelm@48481: wenzelm@48738: session "HOL-Hahn_Banach" in 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@51403: wenzelm@51403: This is the proof of the Hahn-Banach theorem for real vectorspaces, wenzelm@51403: following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach blanchet@55018: theorem is one of the fundamental theorems of functional analysis. It is a wenzelm@51403: conclusion of Zorn's lemma. wenzelm@51403: wenzelm@51403: Two different formaulations of the theorem are presented, one for general wenzelm@51403: real vectorspaces and its application to normed vectorspaces. wenzelm@51403: wenzelm@51403: The theorem says, that every continous linearform, defined on arbitrary wenzelm@51403: subspaces (not only one-dimensional subspaces), can be extended to a wenzelm@51403: continous linearform on the whole vectorspace. wenzelm@48481: *} wenzelm@48481: options [document_graph] wenzelm@48481: theories Hahn_Banach wenzelm@48481: files "document/root.bib" "document/root.tex" wenzelm@48481: wenzelm@48738: session "HOL-Induct" in Induct = HOL + wenzelm@51403: description {* wenzelm@51403: Examples of (Co)Inductive Definitions. wenzelm@51403: wenzelm@51403: Comb proves the Church-Rosser theorem for combinators (see wenzelm@51403: http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz). wenzelm@51403: wenzelm@51403: Mutil is the famous Mutilated Chess Board problem (see wenzelm@51403: http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz). wenzelm@51403: wenzelm@51403: PropLog proves the completeness of a formalization of propositional logic wenzelm@51403: (see wenzelm@51403: HREF="http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz). wenzelm@51403: wenzelm@51403: Exp demonstrates the use of iterated inductive definitions to reason about wenzelm@51403: mutually recursive relations. wenzelm@51403: *} 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@48738: session "HOL-IMP" in IMP = HOL + wenzelm@50870: options [document_graph, document_variants=document] 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" nipkow@51625: "~~/src/HOL/Library/Quotient_List" nipkow@51625: "~~/src/HOL/Library/Extended" wenzelm@48481: theories wenzelm@48481: BExp wenzelm@48481: ASM nipkow@50050: Finite_Reachable nipkow@52394: Denotational nipkow@52400: Compiler2 wenzelm@48481: Poly_Types wenzelm@48481: Sec_Typing wenzelm@48481: Sec_TypingT nipkow@52726: Def_Init_Big nipkow@52726: Def_Init_Small nipkow@52726: Fold wenzelm@48481: Live wenzelm@48481: Live_True wenzelm@48481: Hoare_Examples nipkow@52269: VCG nipkow@52282: Hoare_Total wenzelm@48481: Collecting1 nipkow@48765: Collecting_Examples 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: files "document/root.bib" "document/root.tex" wenzelm@48481: wenzelm@48738: session "HOL-IMPP" in IMPP = HOL + wenzelm@48481: description {* wenzelm@48481: Author: David von Oheimb wenzelm@48481: Copyright 1999 TUM wenzelm@51403: wenzelm@51403: IMPP -- An imperative language with procedures. wenzelm@51403: wenzelm@51403: This is an extension of IMP with local variables and mutually recursive wenzelm@51403: procedures. For documentation see "Hoare Logic for Mutual Recursion and wenzelm@51403: Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html). wenzelm@48481: *} wenzelm@48483: options [document = false] wenzelm@48481: theories EvenOdd wenzelm@48481: wenzelm@48738: session "HOL-Import" in 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@48738: session "HOL-Number_Theory" in Number_Theory = HOL + wenzelm@48483: options [document = false] wenzelm@48481: theories Number_Theory wenzelm@48481: wenzelm@48738: session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL + wenzelm@51403: description {* wenzelm@51403: Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler wenzelm@51403: Theorem, Wilson's Theorem, Quadratic Reciprocity. wenzelm@51403: *} 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@48738: session "HOL-Hoare" in Hoare = HOL + wenzelm@51403: description {* wenzelm@51403: Verification of imperative programs (verification conditions are generated wenzelm@51403: automatically from pre/post conditions and loop invariants). wenzelm@51403: *} wenzelm@51403: wenzelm@48481: theories Hoare wenzelm@48481: files "document/root.bib" "document/root.tex" wenzelm@48481: wenzelm@48738: session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL + wenzelm@51403: description {* wenzelm@51403: Verification of shared-variable imperative programs a la Owicki-Gries. wenzelm@51403: (verification conditions are generated automatically). wenzelm@51403: *} wenzelm@48481: options [document_graph] wenzelm@48481: theories Hoare_Parallel wenzelm@48481: files "document/root.bib" "document/root.tex" wenzelm@48481: wenzelm@48738: session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" + wenzelm@48481: options [document = false, document_graph = false, browser_info = false] wenzelm@51422: theories wenzelm@51422: Generate wenzelm@51422: Generate_Binary_Nat wenzelm@51422: Generate_Target_Nat wenzelm@51422: Generate_Efficient_Datastructures wenzelm@51422: Generate_Pretty_Char wenzelm@48481: wenzelm@48738: session "HOL-Metis_Examples" in 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@48679: options [timeout = 3600, document = false] 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: blanchet@53808: session "HOL-BNF-Nitpick_Examples" in Nitpick_Examples = "HOL-BNF" + wenzelm@48481: description {* wenzelm@48481: Author: Jasmin Blanchette, TU Muenchen wenzelm@48481: Copyright 2009 wenzelm@48481: *} wenzelm@48483: options [document = false] wenzelm@48481: theories [quick_and_dirty] Nitpick_Examples wenzelm@48481: wenzelm@50844: session "HOL-Algebra" (main) in 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: files "document/root.bib" "document/root.tex" wenzelm@48481: wenzelm@48738: session "HOL-Auth" in Auth = HOL + wenzelm@51421: description {* wenzelm@51421: A new approach to verifying authentication protocols. wenzelm@51421: *} 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@51236: session "HOL-UNITY" in UNITY = "HOL-Auth" + wenzelm@48481: description {* wenzelm@48481: Author: Lawrence C Paulson, Cambridge University Computer Laboratory wenzelm@48481: Copyright 1998 University of Cambridge wenzelm@48481: wenzelm@51403: Verifying security protocols using Chandy and Misra's UNITY formalism. wenzelm@48481: *} wenzelm@48481: options [document_graph] 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@48738: session "HOL-Unix" in 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@48738: session "HOL-ZF" in ZF = HOL + wenzelm@48481: theories MainZF Games wenzelm@48481: files "document/root.tex" wenzelm@48481: wenzelm@48738: session "HOL-Imperative_HOL" in Imperative_HOL = HOL + 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/LaTeXsugar" wenzelm@48481: theories Imperative_HOL_ex wenzelm@48481: files "document/root.bib" "document/root.tex" wenzelm@48481: wenzelm@48738: session "HOL-Decision_Procs" in Decision_Procs = HOL + wenzelm@51544: description {* wenzelm@51544: Various decision procedures, typically involving reflection. wenzelm@51544: *} wenzelm@48496: options [condition = ISABELLE_POLYML, document = false] wenzelm@48481: theories Decision_Procs wenzelm@48481: wenzelm@48738: session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" + wenzelm@52499: options [document = false, parallel_proofs = 0] wenzelm@52424: theories wenzelm@52424: Hilbert_Classical wenzelm@52424: XML_Data wenzelm@48481: wenzelm@48738: session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" + wenzelm@51421: description {* wenzelm@51421: Examples for program extraction in Higher-Order Logic. wenzelm@51421: *} wenzelm@52499: options [condition = ISABELLE_POLYML, parallel_proofs = 0] wenzelm@48481: theories [document = false] haftmann@51143: "~~/src/HOL/Library/Code_Target_Numeral" 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@48738: session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" + wenzelm@51403: description {* wenzelm@51403: Lambda Calculus in de Bruijn's Notation. wenzelm@51403: wenzelm@51403: This session defines lambda-calculus terms with de Bruijn indixes and wenzelm@51403: proves confluence of beta, eta and beta+eta. wenzelm@51403: wenzelm@51403: The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole wenzelm@51403: theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html). wenzelm@51403: *} wenzelm@52499: options [document_graph, print_mode = "no_brackets", parallel_proofs = 0] wenzelm@48481: theories [document = false] haftmann@51143: "~~/src/HOL/Library/Code_Target_Int" 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@48738: session "HOL-Prolog" in Prolog = HOL + wenzelm@48481: description {* wenzelm@48481: Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) wenzelm@51403: wenzelm@51403: A bare-bones implementation of Lambda-Prolog. wenzelm@51403: wenzelm@51403: This is a simple exploratory implementation of Lambda-Prolog in HOL, wenzelm@51403: including some minimal examples (in Test.thy) and a more typical example of wenzelm@51403: a little functional language and its type system. wenzelm@48481: *} wenzelm@48483: options [document = false] wenzelm@48481: theories Test Type wenzelm@48481: wenzelm@48738: session "HOL-MicroJava" in MicroJava = HOL + wenzelm@51403: description {* wenzelm@51403: Formalization of a fragment of Java, together with a corresponding virtual wenzelm@51403: machine and a specification of its bytecode verifier and a lightweight wenzelm@51403: bytecode verifier, including proofs of type-safety. wenzelm@51403: *} 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@48738: session "HOL-NanoJava" in NanoJava = HOL + wenzelm@51403: description {* wenzelm@51403: Hoare Logic for a tiny fragment of Java. wenzelm@51403: *} wenzelm@48481: options [document_graph] wenzelm@48481: theories Example wenzelm@48481: files "document/root.bib" "document/root.tex" wenzelm@48481: wenzelm@48738: session "HOL-Bali" in 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@48738: session "HOL-IOA" in IOA = HOL + wenzelm@48481: description {* wenzelm@51403: Author: Tobias Nipkow and Konrad Slind and Olaf Müller wenzelm@51403: Copyright 1994--1996 TU Muenchen wenzelm@48481: wenzelm@51403: The meta theory of I/O-Automata in HOL. This formalization has been wenzelm@51403: significantly changed and extended, see HOLCF/IOA. There are also the wenzelm@51403: proofs of two communication protocols which formerly have been here. 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@48483: options [document = false] wenzelm@48481: theories Solve wenzelm@48481: wenzelm@48738: session "HOL-Lattice" in 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@48738: session "HOL-ex" in ex = HOL + wenzelm@51421: description {* wenzelm@51421: Miscellaneous examples for Higher-Order Logic. wenzelm@51421: *} wenzelm@48679: options [timeout = 3600, condition = ISABELLE_POLYML] wenzelm@48481: theories [document = false] wenzelm@48481: "~~/src/HOL/Library/State_Monad" haftmann@50023: Code_Binary_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" blanchet@49985: "~~/src/HOL/Library/Refute" wenzelm@48481: theories wenzelm@48481: Iff_Oracle wenzelm@48481: Coercion_Examples wenzelm@48481: Higher_Order_Logic wenzelm@48481: Abstract_NAT wenzelm@48481: Guess 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: Termination wenzelm@48481: Coherent wenzelm@48481: PresburgerEx haftmann@51093: Reflection_Examples 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: 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 nipkow@50138: IArray_Examples wenzelm@51559: SVC_Oracle noschinl@53430: Simps_Case_Conv_Examples wenzelm@53935: ML wenzelm@51558: theories [skip_proofs = false] wenzelm@51558: Meson_Test wenzelm@48690: theories [condition = SVC_HOME] wenzelm@48690: 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@48738: session "HOL-Isar_Examples" in Isar_Examples = HOL + wenzelm@51403: description {* wenzelm@51403: Miscellaneous Isabelle/Isar examples for Higher-Order Logic. wenzelm@51403: *} 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@48738: session "HOL-SET_Protocol" in SET_Protocol = HOL + wenzelm@51403: description {* wenzelm@51403: Verification of the SET Protocol. wenzelm@51403: *} 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@48738: session "HOL-Matrix_LP" in Matrix_LP = HOL + wenzelm@51403: description {* wenzelm@51403: Two-dimensional matrices and linear programming. wenzelm@51403: *} wenzelm@48481: options [document_graph] wenzelm@48481: theories Cplex wenzelm@48481: files "document/root.tex" wenzelm@48481: wenzelm@48738: session "HOL-TLA" in TLA = HOL + wenzelm@51403: description {* wenzelm@51403: Lamport's Temporal Logic of Actions. wenzelm@51403: *} wenzelm@48483: options [document = false] wenzelm@48481: theories TLA wenzelm@48481: wenzelm@48738: session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" + wenzelm@48483: options [document = false] wenzelm@48481: theories Inc wenzelm@48481: wenzelm@48738: session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" + wenzelm@48483: options [document = false] wenzelm@48481: theories DBuffer wenzelm@48481: wenzelm@48738: session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" + wenzelm@48483: options [document = false] wenzelm@48481: theories MemoryImplementation wenzelm@48481: wenzelm@48738: session "HOL-TPTP" in 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@48483: options [document = false] 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@52488: theories wenzelm@48481: ATP_Problem_Import wenzelm@48481: wenzelm@50844: session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL + wenzelm@48481: options [document_graph] wenzelm@48481: theories wenzelm@48481: Multivariate_Analysis wenzelm@48481: Determinants wenzelm@48481: files wenzelm@48481: "document/root.tex" wenzelm@48481: wenzelm@48738: session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" + wenzelm@48617: 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@48738: session "HOL-Nominal" (main) in Nominal = HOL + wenzelm@48483: options [document = false] wenzelm@48481: theories Nominal wenzelm@48481: wenzelm@48738: session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" + wenzelm@48679: options [timeout = 3600, condition = ISABELLE_POLYML, document = false] wenzelm@48481: theories Nominal_Examples wenzelm@48481: theories [quick_and_dirty] VC_Condition wenzelm@48481: blanchet@54481: session "HOL-Cardinals-FP" in Cardinals = HOL + wenzelm@51421: description {* blanchet@54481: Ordinals and Cardinals, Theories Needed for BNF FP Constructions. wenzelm@51421: *} blanchet@48975: options [document = false] blanchet@54481: theories Cardinal_Arithmetic_FP blanchet@48975: blanchet@54481: session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-FP" + wenzelm@51421: description {* wenzelm@51421: Ordinals and Cardinals, Full Theories. wenzelm@51421: *} blanchet@49511: options [document = false] popescua@49439: theories Cardinals wenzelm@48984: files wenzelm@48984: "document/intro.tex" wenzelm@48984: "document/root.tex" wenzelm@48984: "document/root.bib" blanchet@48975: blanchet@54481: session "HOL-BNF-FP" in BNF = "HOL-Cardinals-FP" + wenzelm@51421: description {* blanchet@54481: Bounded Natural Functors for (Co)datatypes. wenzelm@51421: *} blanchet@49511: options [document = false] blanchet@54481: theories BNF_LFP BNF_GFP blanchet@49511: blanchet@54481: session "HOL-BNF" in BNF = "HOL-BNF-FP" + blanchet@54474: description {* blanchet@54481: Bounded Natural Functors for (Co)datatypes, Including More BNFs. wenzelm@51421: *} blanchet@48975: options [document = false] blanchet@49510: theories BNF blanchet@48975: blanchet@49510: session "HOL-BNF-Examples" in "BNF/Examples" = "HOL-BNF" + wenzelm@51421: description {* wenzelm@51421: Examples for Bounded Natural Functors. wenzelm@51421: *} wenzelm@49932: options [document = false] blanchet@48975: theories blanchet@48975: Lambda_Term blanchet@48975: Process blanchet@48975: TreeFsetI popescua@49872: "Derivation_Trees/Gram_Lang" popescua@49872: "Derivation_Trees/Parallel" traytel@50517: Koenig traytel@54961: Stream_Processor blanchet@49693: theories [condition = ISABELLE_FULL_TEST] blanchet@53122: Misc_Codatatype blanchet@53122: Misc_Datatype blanchet@54193: Misc_Primcorec blanchet@53306: Misc_Primrec blanchet@48975: wenzelm@50844: session "HOL-Word" (main) in Word = HOL + wenzelm@48481: options [document_graph] wenzelm@48481: theories Word wenzelm@48481: files "document/root.bib" "document/root.tex" wenzelm@48481: wenzelm@48738: session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" + wenzelm@48483: options [document = false] wenzelm@48481: theories WordExamples wenzelm@48481: wenzelm@48738: session "HOL-Statespace" in Statespace = HOL + wenzelm@51558: theories [skip_proofs = false] wenzelm@51558: StateSpaceEx wenzelm@48481: files "document/root.tex" wenzelm@48481: wenzelm@48738: session "HOL-NSA" in NSA = HOL + wenzelm@51421: description {* wenzelm@51421: Nonstandard analysis. wenzelm@51421: *} wenzelm@48481: options [document_graph] wenzelm@48481: theories Hypercomplex wenzelm@48481: files "document/root.tex" wenzelm@48481: wenzelm@48738: session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" + wenzelm@48483: options [document = false] wenzelm@48481: theories NSPrimes wenzelm@48481: wenzelm@48738: session "HOL-Mirabelle" in Mirabelle = HOL + wenzelm@48483: options [document = false] wenzelm@48481: theories Mirabelle_Test wenzelm@48589: wenzelm@48738: session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" + wenzelm@49448: options [document = false, timeout = 60] wenzelm@49448: theories Ex wenzelm@48481: wenzelm@48738: session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" + wenzelm@48483: options [document = false, quick_and_dirty] wenzelm@48481: theories boehmes@52722: Boogie wenzelm@48481: SMT_Examples wenzelm@48481: SMT_Word_Examples blanchet@50666: theories [condition = ISABELLE_FULL_TEST] blanchet@50666: SMT_Tests wenzelm@48481: files wenzelm@48481: "Boogie_Dijkstra.certs" wenzelm@48481: "Boogie_Max.certs" boehmes@52722: "SMT_Examples.certs" boehmes@52722: "SMT_Word_Examples.certs" wenzelm@48481: "VCC_Max.certs" wenzelm@48481: wenzelm@50844: session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" + wenzelm@48483: options [document = false] wenzelm@48481: theories SPARK wenzelm@48481: wenzelm@48738: session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" + wenzelm@48483: options [document = false] 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@48738: session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" + wenzelm@48486: options [show_question_marks = 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@48738: session "HOL-Mutabelle" in Mutabelle = HOL + wenzelm@48483: options [document = false] wenzelm@48481: theories MutabelleExtra wenzelm@48481: wenzelm@48738: session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL + wenzelm@50179: options [document = false] wenzelm@48588: theories wenzelm@48690: Quickcheck_Examples wenzelm@48690: (* FIXME wenzelm@48690: Quickcheck_Lattice_Examples wenzelm@48690: Completeness wenzelm@48690: Quickcheck_Interfaces wenzelm@48690: Hotel_Example *) wenzelm@48598: theories [condition = ISABELLE_GHC] wenzelm@48598: Quickcheck_Narrowing_Examples wenzelm@48588: wenzelm@48738: session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL + wenzelm@50571: theories [condition = ISABELLE_FULL_TEST, quick_and_dirty] bulwahn@50568: Find_Unused_Assms_Examples bulwahn@48618: Needham_Schroeder_No_Attacker_Example bulwahn@48618: Needham_Schroeder_Guided_Attacker_Example wenzelm@48690: Needham_Schroeder_Unguided_Attacker_Example wenzelm@48481: wenzelm@48738: session "HOL-Quotient_Examples" in Quotient_Examples = HOL + wenzelm@48481: description {* wenzelm@48481: Author: Cezary Kaliszyk and Christian Urban wenzelm@48481: *} wenzelm@48483: options [document = false] 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_Fun wenzelm@48481: Quotient_Rat wenzelm@48481: Lift_DList kuncar@53682: Int_Pow wenzelm@48481: wenzelm@48738: session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL + wenzelm@48483: options [document = false] wenzelm@48690: theories wenzelm@48481: Examples wenzelm@48481: Predicate_Compile_Tests wenzelm@48690: (* FIXME wenzelm@48690: Predicate_Compile_Quickcheck_Examples -- should be added again soon (since 21-Oct-2010) *) wenzelm@48481: Specialisation_Examples wenzelm@48690: (* FIXME since 21-Jul-2011 wenzelm@48690: Hotel_Example_Small_Generator wenzelm@48690: IMP_1 wenzelm@48690: IMP_2 wenzelm@48690: IMP_3 wenzelm@48690: IMP_4 *) wenzelm@48690: theories [condition = "ISABELLE_SWIPL"] (* FIXME: *or* ISABELLE_YAP (??) *) wenzelm@48690: Code_Prolog_Examples wenzelm@48690: Context_Free_Grammar_Example wenzelm@48690: Hotel_Example_Prolog wenzelm@48690: Lambda_Example wenzelm@48690: List_Examples wenzelm@48690: theories [condition = "ISABELLE_SWIPL", quick_and_dirty] (* FIXME: *or* ISABELLE_YAP (??) *) wenzelm@48690: Reg_Exp_Example wenzelm@48481: wenzelm@48738: session HOLCF (main) in HOLCF = 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@48738: session "HOLCF-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@48738: session "HOLCF-Library" in "HOLCF/Library" = HOLCF + wenzelm@48483: options [document = false] wenzelm@48481: theories HOLCF_Library wenzelm@48481: wenzelm@48738: session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF + wenzelm@51403: description {* wenzelm@51403: IMP -- A WHILE-language and its Semantics. wenzelm@51403: wenzelm@51403: This is the HOLCF-based denotational semantics of a simple WHILE-language. wenzelm@51403: *} wenzelm@48483: options [document = false] wenzelm@48481: theories HoareEx wenzelm@48338: files "document/root.tex" wenzelm@48338: wenzelm@48738: session "HOLCF-ex" in "HOLCF/ex" = HOLCF + wenzelm@51421: description {* wenzelm@51421: Miscellaneous examples for HOLCF. wenzelm@51421: *} wenzelm@48483: options [document = false] 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@48738: session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF + wenzelm@51403: description {* wenzelm@51403: FOCUS: a theory of stream-processing functions Isabelle/HOLCF. wenzelm@51403: wenzelm@51403: For introductions to FOCUS, see wenzelm@51403: wenzelm@51403: "The Design of Distributed Systems - An Introduction to FOCUS" wenzelm@51403: http://www4.in.tum.de/publ/html.php?e=2 wenzelm@51403: wenzelm@51403: "Specification and Refinement of a Buffer of Length One" wenzelm@51403: http://www4.in.tum.de/publ/html.php?e=15 wenzelm@51403: wenzelm@51403: "Specification and Development of Interactive Systems: Focus on Streams, wenzelm@51403: Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321 wenzelm@51403: *} wenzelm@48483: options [document = false] wenzelm@48481: theories wenzelm@48481: Fstreams wenzelm@48481: FOCUS wenzelm@48481: Buffer_adm wenzelm@48481: wenzelm@48738: session IOA in "HOLCF/IOA" = HOLCF + wenzelm@48481: description {* wenzelm@48481: Author: Olaf Mueller wenzelm@51403: Copyright 1997 TU München wenzelm@48481: wenzelm@51403: A formalization of I/O automata in HOLCF. wenzelm@51403: wenzelm@51403: The distribution contains simulation relations, temporal logic, and an wenzelm@51403: abstraction theory. Everything is based upon a domain-theoretic model of wenzelm@51403: finite and infinite sequences. wenzelm@48481: *} wenzelm@48483: options [document = false] wenzelm@48481: theories "meta_theory/Abstraction" wenzelm@48481: wenzelm@48738: session "IOA-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@48483: options [document = false] wenzelm@48481: theories Correctness wenzelm@48481: wenzelm@48738: session "IOA-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@48483: options [document = false] wenzelm@48481: theories Correctness wenzelm@48481: wenzelm@48738: session "IOA-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@48483: options [document = false] wenzelm@48481: theories Correctness wenzelm@48481: wenzelm@48738: session "IOA-ex" in "HOLCF/IOA/ex" = IOA + wenzelm@48481: description {* wenzelm@48481: Author: Olaf Mueller wenzelm@48481: *} wenzelm@48483: options [document = false] wenzelm@48481: theories wenzelm@48481: TrivEx wenzelm@48481: TrivEx2 wenzelm@48481: wenzelm@48738: session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL + wenzelm@51421: description {* wenzelm@51421: Some rather large datatype examples (from John Harrison). wenzelm@51421: *} wenzelm@48483: options [document = false] wenzelm@48635: theories [condition = ISABELLE_FULL_TEST, timing] wenzelm@48481: Brackin wenzelm@48481: Instructions wenzelm@48481: SML wenzelm@48481: Verilog wenzelm@48481: wenzelm@48738: session "HOL-Record_Benchmark" in Record_Benchmark = HOL + wenzelm@51421: description {* wenzelm@51421: Some benchmark on large record. wenzelm@51421: *} wenzelm@48483: options [document = false] wenzelm@48635: theories [condition = ISABELLE_FULL_TEST, timing] wenzelm@48481: Record_Benchmark wenzelm@48481: