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