--- a/doc-src/ROOT Wed Aug 08 15:58:40 2012 +0200
+++ b/doc-src/ROOT Wed Aug 08 17:49:56 2012 +0200
@@ -1,10 +1,10 @@
-session Classes! (doc) in "Classes/Thy" = HOL +
+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" +
+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"]
@@ -18,12 +18,12 @@
Adaptation
Further
-session Functions! (doc) in "Functions/Thy" = HOL +
+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 +
+session IsarImplementation (doc) in "IsarImplementation/Thy" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex"]
theories
@@ -38,7 +38,7 @@
Syntax
Tactic
-session IsarRef (doc) in "IsarRef/Thy" = HOL +
+session "HOL-IsarRef" (doc) in "IsarRef/Thy" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex",
quick_and_dirty]
@@ -59,19 +59,19 @@
Symbols
ML_Tactic
-session IsarRef (doc) in "IsarRef/Thy" = HOLCF +
+session "HOLCF-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 +
+session "ZF-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 +
+session LaTeXsugar (doc) in "LaTeXsugar/Sugar" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex"]
theories [document_dump = ""]
@@ -79,7 +79,7 @@
"~~/src/HOL/Library/OptionalSugar"
theories Sugar
-session Locales! (doc) in "Locales/Locales" = HOL +
+session Locales (doc) in "Locales/Locales" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex"]
theories
@@ -87,12 +87,12 @@
Examples2
Examples3
-session Main! (doc) in "Main/Docs" = HOL +
+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 +
+session ProgProve (doc) in "ProgProve/Thys" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex",
show_question_marks = false]
@@ -104,7 +104,7 @@
Logic
Isar
-session System! (doc) in "System/Thy" = Pure +
+session System (doc) in "System/Thy" = Pure +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex"]
theories
@@ -177,11 +177,11 @@
"Sets/Relations"
"Sets/Recur"
-session ToyList2 (doc) in "TutorialI/ToyList2" = HOL +
+session "HOL-ToyList2" (doc) in "TutorialI/ToyList2" = HOL +
options [browser_info = false, document = false, print_mode = "brackets"]
theories ToyList
-session examples (doc) in "ZF" = ZF +
+session "ZF-examples" (doc) in "ZF" = ZF +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex",
print_mode = "brackets"]