session Classes! (doc) in "Classes/Thy" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex"]
theories [document = false] Setup
theories Classes
session Codegen! (doc) in "Codegen/Thy" = "HOL-Library" +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex",
print_mode = "no_brackets,iff"]
theories [document = false] Setup
theories
Introduction
Foundations
Refinement
Inductive_Predicate
Evaluation
Adaptation
Further
session Functions! (doc) in "Functions/Thy" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex"]
theories Functions
session IsarImplementation! (doc) in "IsarImplementation/Thy" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex"]
theories
Eq
Integration
Isar
Local_Theory
Logic
ML
Prelim
Proof
Syntax
Tactic
session IsarRef (doc) in "IsarRef/Thy" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex",
quick_and_dirty]
theories
Preface
Synopsis
Framework
First_Order_Logic
Outer_Syntax
Document_Preparation
Spec
Proof
Inner_Syntax
Misc
Generic
HOL_Specific
Quick_Reference
Symbols
ML_Tactic
session IsarRef (doc) in "IsarRef/Thy" = HOLCF +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex",
quick_and_dirty]
theories HOLCF_Specific
session IsarRef (doc) in "IsarRef/Thy" = ZF +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex",
quick_and_dirty]
theories ZF_Specific
session LaTeXsugar! (doc) in "LaTeXsugar/Sugar" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex"]
theories [document_dump = ""]
"~~/src/HOL/Library/LaTeXsugar"
"~~/src/HOL/Library/OptionalSugar"
theories Sugar
session Locales! (doc) in "Locales/Locales" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex"]
theories
Examples1
Examples2
Examples3
session Main! (doc) in "Main/Docs" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex"]
theories Main_Doc
session ProgProve! (doc) in "ProgProve/Thys" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex",
show_question_marks = false]
theories
Basics
Bool_nat_list
MyList
Types_and_funs
Logic
Isar
session System! (doc) in "System/Thy" = Pure +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex"]
theories
Basics
Interfaces
Sessions
Presentation
Scala
Misc
session Tutorial (doc) in "TutorialI" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex",
print_mode = "brackets", threads = 1 (* FIXME *)]
theories [thy_output_indent = 5]
"ToyList/ToyList"
"Ifexpr/Ifexpr"
"CodeGen/CodeGen"
"Trie/Trie"
"Datatype/ABexpr"
"Datatype/unfoldnested"
"Datatype/Nested"
"Datatype/Fundata"
"Fun/fun0"
"Advanced/simp2"
"CTL/PDL"
"CTL/CTL"
"CTL/CTLind"
"Inductive/Even"
"Inductive/Mutual"
"Inductive/Star"
"Inductive/AB"
"Inductive/Advanced"
"Misc/Tree"
"Misc/Tree2"
"Misc/Plus"
"Misc/case_exprs"
"Misc/fakenat"
"Misc/natsum"
"Misc/pairs2"
"Misc/Option2"
"Misc/types"
"Misc/prime_def"
"Misc/simp"
"Misc/Itrev"
"Misc/AdvancedInd"
"Misc/appendix"
theories
"Protocol/NS_Public"
"Documents/Documents"
theories [document_dump = ""]
"Types/Setup"
theories
"Types/Numbers"
"Types/Pairs"
"Types/Records"
"Types/Typedefs"
"Types/Overloading"
"Types/Axioms"
"Rules/Basic"
"Rules/Blast"
"Rules/Force"
"Rules/Forward"
"Rules/Tacticals"
"Rules/find2"
"Sets/Examples"
"Sets/Functions"
"Sets/Relations"
"Sets/Recur"
session examples (doc) in "ZF" = ZF +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex",
print_mode = "brackets"]
theories
IFOL_examples
FOL_examples
ZF_examples
If