chapter Doc
session Classes (doc) in "Classes" = HOL +
options [document_variants = "classes", quick_and_dirty]
theories [document = false] Setup
theories Classes
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
"iman.sty"
"extra.sty"
"isar.sty"
"manual.bib"
document_files
"build"
"root.tex"
"style.sty"
session Codegen (doc) in "Codegen" = HOL +
options [document_variants = "codegen", print_mode = "no_brackets,iff"]
sessions
"HOL-Library"
theories [document = false]
Setup
theories
Introduction
Foundations
Refinement
Inductive_Predicate
Evaluation
Computations
Adaptation
Further
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
"iman.sty"
"extra.sty"
"isar.sty"
"manual.bib"
document_files
"build"
"root.tex"
"style.sty"
session Corec (doc) in "Corec" = Datatypes +
options [document_variants = "corec"]
theories
Corec
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
"iman.sty"
"extra.sty"
"isar.sty"
"manual.bib"
document_files
"build"
"root.tex"
"style.sty"
session Datatypes (doc) in "Datatypes" = HOL +
options [document_variants = "datatypes"]
sessions
"HOL-Library"
theories [document = false]
Setup
theories
Datatypes
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
"iman.sty"
"extra.sty"
"isar.sty"
"manual.bib"
document_files
"build"
"root.tex"
"style.sty"
session Eisbach (doc) in "Eisbach" = HOL +
options [document_variants = "eisbach", quick_and_dirty,
print_mode = "no_brackets,iff", show_question_marks = false]
sessions
"HOL-Eisbach"
theories [document = false]
Base
theories
Preface
Manual
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
"iman.sty"
"extra.sty"
"isar.sty"
"ttbox.sty"
"underscore.sty"
"manual.bib"
document_files
"build"
"root.tex"
"style.sty"
session Functions (doc) in "Functions" = HOL +
options [document_variants = "functions", skip_proofs = false, quick_and_dirty]
theories Functions
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
"iman.sty"
"extra.sty"
"isar.sty"
"manual.bib"
document_files
"build"
"conclusion.tex"
"intro.tex"
"root.tex"
"style.sty"
session How_to_Prove_it (no_doc) in "How_to_Prove_it" = HOL +
options [document_variants = "how_to_prove_it", show_question_marks = false]
theories
How_to_Prove_it
document_files
"root.tex"
"root.bib"
"prelude.tex"
session Intro (doc) in "Intro" = Pure +
options [document_variants = "intro"]
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
"iman.sty"
"extra.sty"
"ttbox.sty"
"manual.bib"
document_files
"advanced.tex"
"build"
"foundations.tex"
"getting.tex"
"root.tex"
session Implementation (doc) in "Implementation" = HOL +
options [document_variants = "implementation", quick_and_dirty]
theories
Eq
Integration
Isar
Local_Theory
"ML"
Prelim
Proof
Syntax
Tactic
theories [parallel_proofs = 0]
Logic
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
"iman.sty"
"extra.sty"
"isar.sty"
"ttbox.sty"
"underscore.sty"
"manual.bib"
document_files
"build"
"root.tex"
"style.sty"
session Isar_Ref (doc) in "Isar_Ref" = HOL +
options [document_variants = "isar-ref", quick_and_dirty, thy_output_source]
sessions
"HOL-Library"
theories
Preface
Synopsis
Framework
First_Order_Logic
Outer_Syntax
Document_Preparation
Spec
Proof
Proof_Script
Inner_Syntax
Generic
HOL_Specific
Quick_Reference
Symbols
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
"iman.sty"
"extra.sty"
"isar.sty"
"ttbox.sty"
"underscore.sty"
"manual.bib"
document_files
"build"
"isar-vm.pdf"
"isar-vm.svg"
"root.tex"
"showsymbols"
"style.sty"
session JEdit (doc) in "JEdit" = HOL +
options [document_variants = "jedit", thy_output_source]
theories
JEdit
document_files (in "..")
"extra.sty"
"iman.sty"
"isar.sty"
"manual.bib"
"pdfsetup.sty"
"prepare_document"
"ttbox.sty"
"underscore.sty"
document_files (in "../Isar_Ref/document")
"style.sty"
document_files
"auto-tools.png"
"bibtex-mode.png"
"build"
"cite-completion.png"
"isabelle-jedit-hdpi.png"
"isabelle-jedit.png"
"markdown-document.png"
"ml-debugger.png"
"output-and-state.png"
"output-including-state.png"
"output.png"
"popup1.png"
"popup2.png"
"query.png"
"root.tex"
"scope1.png"
"scope2.png"
"sidekick-document.png"
"sidekick.png"
"sledgehammer.png"
"theories.png"
session Sugar (doc) in "Sugar" = HOL +
options [document_variants = "sugar"]
sessions
"HOL-Library"
theories Sugar
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
document_files
"build"
"root.bib"
"root.tex"
session Locales (doc) in "Locales" = HOL +
options [document_variants = "locales", thy_output_margin = 65, skip_proofs = false]
theories
Examples1
Examples2
Examples3
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
document_files
"build"
"root.bib"
"root.tex"
session Logics (doc) in "Logics" = Pure +
options [document_variants = "logics"]
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
"iman.sty"
"extra.sty"
"ttbox.sty"
"manual.bib"
document_files
"CTT.tex"
"HOL.tex"
"LK.tex"
"Sequents.tex"
"build"
"preface.tex"
"root.tex"
"syntax.tex"
session Logics_ZF (doc) in "Logics_ZF" = ZF +
options [document_variants = "logics-ZF", print_mode = "brackets",
thy_output_source]
sessions
FOL
theories
IFOL_examples
FOL_examples
ZF_examples
If
ZF_Isar
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
"isar.sty"
"ttbox.sty"
"manual.bib"
document_files (in "../Logics/document")
"syntax.tex"
document_files
"FOL.tex"
"ZF.tex"
"build"
"logics.sty"
"root.tex"
session Main (doc) in "Main" = HOL +
options [document_variants = "main"]
theories Main_Doc
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
document_files
"build"
"root.tex"
session Nitpick (doc) in "Nitpick" = Pure +
options [document_variants = "nitpick"]
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
"iman.sty"
"manual.bib"
document_files
"build"
"root.tex"
session Prog_Prove (doc) in "Prog_Prove" = HOL +
options [document_variants = "prog-prove", show_question_marks = false]
theories
Basics
Bool_nat_list
MyList
Types_and_funs
Logic
Isar
document_files (in ".")
"MyList.thy"
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
document_files
"bang.pdf"
"build"
"intro-isabelle.tex"
"prelude.tex"
"root.bib"
"root.tex"
"svmono.cls"
session Sledgehammer (doc) in "Sledgehammer" = Pure +
options [document_variants = "sledgehammer"]
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
"iman.sty"
"manual.bib"
document_files
"build"
"root.tex"
session System (doc) in "System" = Pure +
options [document_variants = "system", thy_output_source]
sessions
"HOL-Library"
theories
Environment
Sessions
Presentation
Server
Scala
Phabricator
Misc
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
"iman.sty"
"extra.sty"
"isar.sty"
"ttbox.sty"
"underscore.sty"
"manual.bib"
document_files (in "../Isar_Ref/document")
"style.sty"
document_files
"build"
"root.tex"
session Tutorial (doc) in "Tutorial" = HOL +
options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
directories "Advanced" "CTL" "CodeGen" "Datatype" "Documents" "Fun" "Ifexpr"
"Inductive" "Misc" "Protocol" "Rules" "Sets" "ToyList" "Trie" "Types"
theories [threads = 1]
"ToyList/ToyList_Test"
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 = false]
"Types/Setup"
theories [thy_output_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 [thy_output_margin = 64, thy_output_indent = 5]
"Rules/TPrimes"
"Rules/Forward"
"Rules/Tacticals"
"Rules/find2"
"Sets/Examples"
"Sets/Functions"
"Sets/Relations"
"Sets/Recur"
document_files (in "ToyList")
"ToyList1.txt"
"ToyList2.txt"
document_files (in "..")
"pdfsetup.sty"
"ttbox.sty"
"manual.bib"
document_files
"advanced0.tex"
"appendix0.tex"
"basics.tex"
"build"
"cl2emono-modified.sty"
"ctl0.tex"
"documents0.tex"
"fp.tex"
"inductive0.tex"
"isa-index"
"Isa-logics.pdf"
"numerics.tex"
"pghead.pdf"
"preface.tex"
"protocol.tex"
"root.tex"
"rules.tex"
"sets.tex"
"tutorial.sty"
"typedef.pdf"
"types0.tex"
session Typeclass_Hierarchy (doc) in "Typeclass_Hierarchy" = HOL +
options [document_variants = "typeclass_hierarchy"]
sessions
"HOL-Library"
theories [document = false]
Setup
theories
Typeclass_Hierarchy
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
"iman.sty"
"extra.sty"
"isar.sty"
"manual.bib"
document_files
"build"
"root.tex"
"style.sty"