session Classes (doc) in "Classes" = HOL +
options [document_variants = "classes"]
theories [document = false] Setup
theories Classes
files
"../pdfsetup.sty"
"document/build"
"document/root.tex"
"document/style.sty"
session Codegen (doc) in "Codegen" = "HOL-Library" +
options [document_variants = "codegen", print_mode = "no_brackets,iff"]
theories [document = false] Setup
theories
Introduction
Foundations
Refinement
Inductive_Predicate
Evaluation
Adaptation
Further
files
"../pdfsetup.sty"
"document/adapt.tex"
"document/architecture.tex"
"document/build"
"document/root.tex"
"document/style.sty"
session Functions (doc) in "Functions" = HOL +
options [document_variants = "functions"]
theories Functions
files
"../pdfsetup.sty"
"../iman.sty"
"../extra.sty"
"../isar.sty"
"../manual.bib"
"document/build"
"document/conclusion.tex"
"document/intro.tex"
"document/mathpartir.sty"
"document/root.tex"
"document/style.sty"
session IsarImplementation (doc) in "IsarImplementation" = HOL +
options [document_variants = "implementation"]
theories
Eq
Integration
Isar
Local_Theory
Logic
ML
Prelim
Proof
Syntax
Tactic
files
"../pdfsetup.sty"
"../iman.sty"
"../extra.sty"
"../isar.sty"
"../proof.sty"
"../underscore.sty"
"../ttbox.sty"
"../manual.bib"
"document/build"
"document/root.tex"
"document/style.sty"
session Intro (doc) in "Intro" = Pure +
options [document_variants = "intro"]
theories
files
"../pdfsetup.sty"
"../iman.sty"
"../extra.sty"
"../ttbox.sty"
"../proof.sty"
"../manual.bib"
"document/build"
"document/root.tex"
session IsarRef (doc) in "IsarRef" = HOL +
options [document_variants = "isar-ref", quick_and_dirty, thy_output_source]
theories
Preface
Synopsis
Framework
First_Order_Logic
Outer_Syntax
Document_Preparation
Spec
Proof
Inner_Syntax
Misc
Generic
HOL_Specific
Quick_Reference
Symbols
ML_Tactic
files
"../pdfsetup.sty"
"../iman.sty"
"../extra.sty"
"../ttbox.sty"
"../proof.sty"
"../isar.sty"
"../manual.bib"
"document/build"
"document/isar-vm.eps"
"document/isar-vm.pdf"
"document/isar-vm.svg"
"document/root.tex"
"document/showsymbols"
"document/style.sty"
session LaTeXsugar (doc) in "LaTeXsugar" = HOL +
options [document_variants = "sugar"]
theories [document = ""]
"~~/src/HOL/Library/LaTeXsugar"
"~~/src/HOL/Library/OptionalSugar"
theories Sugar
files
"../pdfsetup.sty"
"document/build"
"document/mathpartir.sty"
"document/root.bib"
"document/root.tex"
session Locales (doc) in "Locales" = HOL +
options [document_variants = "locales", pretty_margin = 65]
theories
Examples1
Examples2
Examples3
files
"../pdfsetup.sty"
"document/build"
"document/root.tex"
session Logics (doc) in "Logics" = Pure +
options [document_variants = "logics"]
theories
files
"../pdfsetup.sty"
"../iman.sty"
"../extra.sty"
"../ttbox.sty"
"../proof.sty"
"../manual.bib"
"document/build"
"document/root.tex"
session "Logics-HOL" (doc) in "HOL" = Pure +
options [document_variants = "logics-HOL"]
theories
files
"../pdfsetup.sty"
"../iman.sty"
"../extra.sty"
"../ttbox.sty"
"../proof.sty"
"../manual.bib"
"../Logics/document/syntax.tex"
"document/build"
"document/root.tex"
session "Logics-ZF" (doc) in "ZF" = ZF +
options [document_variants = "logics-ZF", print_mode = "brackets",
thy_output_source]
theories
IFOL_examples
FOL_examples
ZF_examples
If
ZF_Isar
files
"../pdfsetup.sty"
"../isar.sty"
"../ttbox.sty"
"../proof.sty"
"../manual.bib"
"../Logics/document/syntax.tex"
"document/build"
"document/root.tex"
session Main (doc) in "Main" = HOL +
options [document_variants = "main"]
theories Main_Doc
files
"../pdfsetup.sty"
"document/build"
"document/root.tex"
session ProgProve (doc) in "ProgProve" = HOL +
options [document_variants = "prog-prove", show_question_marks = false]
theories
Basics
Bool_nat_list
MyList
Types_and_funs
Logic
Isar
files
"../pdfsetup.sty"
"document/bang.eps"
"document/bang.pdf"
"document/build"
"document/intro-isabelle.tex"
"document/mathpartir.sty"
"document/prelude.tex"
"document/root.bib"
"document/root.tex"
"document/svmono.cls"
session Ref (doc) in "Ref" = Pure +
options [document_variants = "ref"]
theories
files
"../pdfsetup.sty"
"../iman.sty"
"../extra.sty"
"../ttbox.sty"
"../proof.sty"
"../manual.bib"
"document/build"
"document/classical.tex"
"document/root.tex"
"document/simplifier.tex"
"document/substitution.tex"
"document/syntax.tex"
"document/tactic.tex"
"document/thm.tex"
session System (doc) in "System" = Pure +
options [document_variants = "system", thy_output_source]
theories
Basics
Interfaces
Sessions
Presentation
Scala
Misc
files
"../IsarRef/style.sty"
"../pdfsetup.sty"
"../iman.sty"
"../extra.sty"
"../ttbox.sty"
"../isar.sty"
"../underscore.sty"
"../manual.bib"
"document/browser_screenshot.eps"
"document/browser_screenshot.png"
"document/build"
"document/root.tex"
session Tutorial (doc) in "TutorialI" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex",
print_mode = "brackets"]
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 [pretty_margin = 64, thy_output_indent = 0]
"Types/Numbers"
"Types/Pairs"
"Types/Records"
"Types/Typedefs"
"Types/Overloading"
"Types/Axioms"
"Rules/Basic"
"Rules/Blast"
"Rules/Force"
theories [pretty_margin = 64, thy_output_indent = 5]
"Rules/Primes"
"Rules/Forward"
"Rules/Tacticals"
"Rules/find2"
"Sets/Examples"
"Sets/Functions"
"Sets/Relations"
"Sets/Recur"
session "HOL-ToyList2" (doc) in "TutorialI/ToyList2" = HOL +
options [browser_info = false, document = false, print_mode = "brackets"]
theories ToyList