1chapter Doc 2 3session Classes (doc) in "Classes" = HOL + 4 options [document_variants = "classes", quick_and_dirty] 5 theories [document = false] Setup 6 theories Classes 7 document_files (in "..") 8 "prepare_document" 9 "pdfsetup.sty" 10 "iman.sty" 11 "extra.sty" 12 "isar.sty" 13 "manual.bib" 14 document_files 15 "build" 16 "root.tex" 17 "style.sty" 18 19session Codegen_Basics in "Codegen" = "HOL-Library" + 20 theories 21 Setup 22 23session Codegen (doc) in "Codegen" = "Codegen_Basics" + 24 options [document_variants = "codegen", print_mode = "no_brackets,iff"] 25 theories 26 Introduction 27 Foundations 28 Refinement 29 Inductive_Predicate 30 Evaluation 31 Computations 32 Adaptation 33 Further 34 document_files (in "..") 35 "prepare_document" 36 "pdfsetup.sty" 37 "iman.sty" 38 "extra.sty" 39 "isar.sty" 40 "manual.bib" 41 document_files 42 "build" 43 "root.tex" 44 "style.sty" 45 46session Corec (doc) in "Corec" = "HOL-Library" + 47 options [document_variants = "corec"] 48 sessions 49 Datatypes 50 theories Corec 51 document_files (in "..") 52 "prepare_document" 53 "pdfsetup.sty" 54 "iman.sty" 55 "extra.sty" 56 "isar.sty" 57 "manual.bib" 58 document_files 59 "build" 60 "root.tex" 61 "style.sty" 62 63session Datatypes (doc) in "Datatypes" = "HOL-Library" + 64 options [document_variants = "datatypes"] 65 theories [document = false] Setup 66 theories Datatypes 67 document_files (in "..") 68 "prepare_document" 69 "pdfsetup.sty" 70 "iman.sty" 71 "extra.sty" 72 "isar.sty" 73 "manual.bib" 74 document_files 75 "build" 76 "root.tex" 77 "style.sty" 78 79session Eisbach (doc) in "Eisbach" = "HOL-Eisbach" + 80 options [document_variants = "eisbach", quick_and_dirty, 81 print_mode = "no_brackets,iff", show_question_marks = false] 82 theories [document = false] 83 Base 84 theories 85 Preface 86 Manual 87 document_files (in "..") 88 "prepare_document" 89 "pdfsetup.sty" 90 "iman.sty" 91 "extra.sty" 92 "isar.sty" 93 "ttbox.sty" 94 "underscore.sty" 95 "manual.bib" 96 document_files 97 "build" 98 "root.tex" 99 "style.sty" 100 101session Functions (doc) in "Functions" = HOL + 102 options [document_variants = "functions", skip_proofs = false, quick_and_dirty] 103 theories Functions 104 document_files (in "..") 105 "prepare_document" 106 "pdfsetup.sty" 107 "iman.sty" 108 "extra.sty" 109 "isar.sty" 110 "manual.bib" 111 document_files 112 "build" 113 "conclusion.tex" 114 "intro.tex" 115 "mathpartir.sty" 116 "root.tex" 117 "style.sty" 118 119session How_to_Prove_it (* FIXME (doc) *) in "How_to_Prove_it" = HOL + 120 options [document_variants = "how_to_prove_it", show_question_marks = false] 121 theories 122 How_to_Prove_it 123 document_files 124 "root.tex" 125 "root.bib" 126 "prelude.tex" 127 128session Intro (doc) in "Intro" = Pure + 129 options [document_variants = "intro"] 130 document_files (in "..") 131 "prepare_document" 132 "pdfsetup.sty" 133 "iman.sty" 134 "extra.sty" 135 "ttbox.sty" 136 "manual.bib" 137 document_files 138 "advanced.tex" 139 "build" 140 "foundations.tex" 141 "getting.tex" 142 "root.tex" 143 144session Implementation (doc) in "Implementation" = "HOL" + 145 options [document_variants = "implementation", quick_and_dirty] 146 theories 147 Eq 148 Integration 149 Isar 150 Local_Theory 151 "ML" 152 Prelim 153 Proof 154 Syntax 155 Tactic 156 theories [parallel_proofs = 0] 157 Logic 158 document_files (in "..") 159 "prepare_document" 160 "pdfsetup.sty" 161 "iman.sty" 162 "extra.sty" 163 "isar.sty" 164 "ttbox.sty" 165 "underscore.sty" 166 "manual.bib" 167 document_files 168 "build" 169 "root.tex" 170 "style.sty" 171 172session Isar_Ref (doc) in "Isar_Ref" = "HOL-Library" + 173 options [document_variants = "isar-ref", quick_and_dirty, thy_output_source] 174 theories 175 Preface 176 Synopsis 177 Framework 178 First_Order_Logic 179 Outer_Syntax 180 Document_Preparation 181 Spec 182 Proof 183 Proof_Script 184 Inner_Syntax 185 Generic 186 HOL_Specific 187 Quick_Reference 188 Symbols 189 document_files (in "..") 190 "prepare_document" 191 "pdfsetup.sty" 192 "iman.sty" 193 "extra.sty" 194 "isar.sty" 195 "ttbox.sty" 196 "underscore.sty" 197 "manual.bib" 198 document_files 199 "build" 200 "isar-vm.pdf" 201 "isar-vm.svg" 202 "root.tex" 203 "showsymbols" 204 "style.sty" 205 206session JEdit (doc) in "JEdit" = HOL + 207 options [document_variants = "jedit", thy_output_source] 208 theories 209 JEdit 210 document_files (in "..") 211 "extra.sty" 212 "iman.sty" 213 "isar.sty" 214 "manual.bib" 215 "pdfsetup.sty" 216 "prepare_document" 217 "ttbox.sty" 218 "underscore.sty" 219 document_files (in "../Isar_Ref/document") 220 "style.sty" 221 document_files 222 "auto-tools.png" 223 "bibtex-mode.png" 224 "build" 225 "cite-completion.png" 226 "isabelle-jedit-hdpi.png" 227 "isabelle-jedit.png" 228 "markdown-document.png" 229 "ml-debugger.png" 230 "output-and-state.png" 231 "output-including-state.png" 232 "output.png" 233 "popup1.png" 234 "popup2.png" 235 "query.png" 236 "root.tex" 237 "scope1.png" 238 "scope2.png" 239 "sidekick-document.png" 240 "sidekick.png" 241 "sledgehammer.png" 242 "theories.png" 243 244session Sugar (doc) in "Sugar" = HOL + 245 options [document_variants = "sugar"] 246 sessions 247 "HOL-Library" 248 theories Sugar 249 document_files (in "..") 250 "prepare_document" 251 "pdfsetup.sty" 252 document_files 253 "build" 254 "mathpartir.sty" 255 "root.bib" 256 "root.tex" 257 258session Locales (doc) in "Locales" = HOL + 259 options [document_variants = "locales", thy_output_margin = 65, skip_proofs = false] 260 theories 261 Examples1 262 Examples2 263 Examples3 264 document_files (in "..") 265 "prepare_document" 266 "pdfsetup.sty" 267 document_files 268 "build" 269 "root.bib" 270 "root.tex" 271 272session Logics (doc) in "Logics" = Pure + 273 options [document_variants = "logics"] 274 document_files (in "..") 275 "prepare_document" 276 "pdfsetup.sty" 277 "iman.sty" 278 "extra.sty" 279 "ttbox.sty" 280 "manual.bib" 281 document_files 282 "CTT.tex" 283 "HOL.tex" 284 "LK.tex" 285 "Sequents.tex" 286 "build" 287 "preface.tex" 288 "root.tex" 289 "syntax.tex" 290 291session Logics_ZF (doc) in "Logics_ZF" = ZF + 292 options [document_variants = "logics-ZF", print_mode = "brackets", 293 thy_output_source] 294 sessions 295 FOL 296 theories 297 IFOL_examples 298 FOL_examples 299 ZF_examples 300 If 301 ZF_Isar 302 document_files (in "..") 303 "prepare_document" 304 "pdfsetup.sty" 305 "isar.sty" 306 "ttbox.sty" 307 "manual.bib" 308 document_files (in "../Logics/document") 309 "syntax.tex" 310 document_files 311 "FOL.tex" 312 "ZF.tex" 313 "build" 314 "logics.sty" 315 "root.tex" 316 317session Main (doc) in "Main" = HOL + 318 options [document_variants = "main"] 319 theories Main_Doc 320 document_files (in "..") 321 "prepare_document" 322 "pdfsetup.sty" 323 document_files 324 "build" 325 "root.tex" 326 327session Nitpick (doc) in "Nitpick" = Pure + 328 options [document_variants = "nitpick"] 329 document_files (in "..") 330 "prepare_document" 331 "pdfsetup.sty" 332 "iman.sty" 333 "manual.bib" 334 document_files 335 "build" 336 "root.tex" 337 338session Prog_Prove (doc) in "Prog_Prove" = HOL + 339 options [document_variants = "prog-prove", show_question_marks = false] 340 theories 341 Basics 342 Bool_nat_list 343 MyList 344 Types_and_funs 345 Logic 346 Isar 347 document_files (in ".") 348 "MyList.thy" 349 document_files (in "..") 350 "prepare_document" 351 "pdfsetup.sty" 352 document_files 353 "bang.pdf" 354 "build" 355 "intro-isabelle.tex" 356 "mathpartir.sty" 357 "prelude.tex" 358 "root.bib" 359 "root.tex" 360 "svmono.cls" 361 362session Sledgehammer (doc) in "Sledgehammer" = Pure + 363 options [document_variants = "sledgehammer"] 364 document_files (in "..") 365 "prepare_document" 366 "pdfsetup.sty" 367 "iman.sty" 368 "manual.bib" 369 document_files 370 "build" 371 "root.tex" 372 373session System (doc) in "System" = Pure + 374 options [document_variants = "system", thy_output_source] 375 sessions 376 "HOL-Library" 377 theories 378 Environment 379 Sessions 380 Presentation 381 Server 382 Scala 383 Misc 384 document_files (in "..") 385 "prepare_document" 386 "pdfsetup.sty" 387 "iman.sty" 388 "extra.sty" 389 "isar.sty" 390 "ttbox.sty" 391 "underscore.sty" 392 "manual.bib" 393 document_files (in "../Isar_Ref/document") 394 "style.sty" 395 document_files 396 "build" 397 "root.tex" 398 399session Tutorial (doc) in "Tutorial" = HOL + 400 options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false] 401 theories [threads = 1] 402 "ToyList/ToyList_Test" 403 theories [thy_output_indent = 5] 404 "ToyList/ToyList" 405 "Ifexpr/Ifexpr" 406 "CodeGen/CodeGen" 407 "Trie/Trie" 408 "Datatype/ABexpr" 409 "Datatype/unfoldnested" 410 "Datatype/Nested" 411 "Datatype/Fundata" 412 "Fun/fun0" 413 "Advanced/simp2" 414 "CTL/PDL" 415 "CTL/CTL" 416 "CTL/CTLind" 417 "Inductive/Even" 418 "Inductive/Mutual" 419 "Inductive/Star" 420 "Inductive/AB" 421 "Inductive/Advanced" 422 "Misc/Tree" 423 "Misc/Tree2" 424 "Misc/Plus" 425 "Misc/case_exprs" 426 "Misc/fakenat" 427 "Misc/natsum" 428 "Misc/pairs2" 429 "Misc/Option2" 430 "Misc/types" 431 "Misc/prime_def" 432 "Misc/simp" 433 "Misc/Itrev" 434 "Misc/AdvancedInd" 435 "Misc/appendix" 436 theories 437 "Protocol/NS_Public" 438 "Documents/Documents" 439 theories [document = false] 440 "Types/Setup" 441 theories [thy_output_margin = 64, thy_output_indent = 0] 442 "Types/Numbers" 443 "Types/Pairs" 444 "Types/Records" 445 "Types/Typedefs" 446 "Types/Overloading" 447 "Types/Axioms" 448 "Rules/Basic" 449 "Rules/Blast" 450 "Rules/Force" 451 theories [thy_output_margin = 64, thy_output_indent = 5] 452 "Rules/TPrimes" 453 "Rules/Forward" 454 "Rules/Tacticals" 455 "Rules/find2" 456 "Sets/Examples" 457 "Sets/Functions" 458 "Sets/Relations" 459 "Sets/Recur" 460 document_files (in "ToyList") 461 "ToyList1.txt" 462 "ToyList2.txt" 463 document_files (in "..") 464 "pdfsetup.sty" 465 "ttbox.sty" 466 "manual.bib" 467 document_files 468 "advanced0.tex" 469 "appendix0.tex" 470 "basics.tex" 471 "build" 472 "cl2emono-modified.sty" 473 "ctl0.tex" 474 "documents0.tex" 475 "fp.tex" 476 "inductive0.tex" 477 "isa-index" 478 "Isa-logics.pdf" 479 "numerics.tex" 480 "pghead.pdf" 481 "preface.tex" 482 "protocol.tex" 483 "root.tex" 484 "rules.tex" 485 "sets.tex" 486 "tutorial.sty" 487 "typedef.pdf" 488 "types0.tex" 489 490session Typeclass_Hierarchy (doc) in "Typeclass_Hierarchy" = "Typeclass_Hierarchy_Basics" + 491 options [document_variants = "typeclass_hierarchy"] 492 theories Typeclass_Hierarchy 493 document_files (in "..") 494 "prepare_document" 495 "pdfsetup.sty" 496 "iman.sty" 497 "extra.sty" 498 "isar.sty" 499 "manual.bib" 500 document_files 501 "build" 502 "root.tex" 503 "style.sty" 504 505session Typeclass_Hierarchy_Basics in "Typeclass_Hierarchy" = "HOL-Library" + 506 theories 507 Setup 508