src/Doc/ROOT
author wenzelm
Sun Jul 07 20:23:09 2013 +0200 (2013-07-07)
changeset 52552 0260bdba4dd7
parent 52499 812215680f6d
child 52741 c08bd0a219f8
permissions -rw-r--r--
reduced number of old manuals: chapter HOL is back again to the Logics manual by Larry;
     1 chapter Doc
     2 
     3 session Classes (doc) in "Classes" = HOL +
     4   options [document_variants = "classes"]
     5   theories [document = false] Setup
     6   theories Classes
     7   files
     8     "../prepare_document"
     9     "../pdfsetup.sty"
    10     "../iman.sty"
    11     "../extra.sty"
    12     "../isar.sty"
    13     "../manual.bib"
    14     "document/build"
    15     "document/root.tex"
    16     "document/style.sty"
    17 
    18 session Codegen (doc) in "Codegen" = "HOL-Library" +
    19   options [document_variants = "codegen", print_mode = "no_brackets,iff"]
    20   theories [document = false] Setup
    21   theories
    22     Introduction
    23     Foundations
    24     Refinement
    25     Inductive_Predicate
    26     Evaluation
    27     Adaptation
    28     Further
    29   files
    30     "../prepare_document"
    31     "../pdfsetup.sty"
    32     "../iman.sty"
    33     "../extra.sty"
    34     "../isar.sty"
    35     "../manual.bib"
    36     "document/adapt.tex"
    37     "document/architecture.tex"
    38     "document/build"
    39     "document/root.tex"
    40     "document/style.sty"
    41 
    42 session Functions (doc) in "Functions" = HOL +
    43   options [document_variants = "functions", skip_proofs = false]
    44   theories Functions
    45   files
    46     "../prepare_document"
    47     "../pdfsetup.sty"
    48     "../iman.sty"
    49     "../extra.sty"
    50     "../isar.sty"
    51     "../manual.bib"
    52     "document/build"
    53     "document/conclusion.tex"
    54     "document/intro.tex"
    55     "document/mathpartir.sty"
    56     "document/root.tex"
    57     "document/style.sty"
    58 
    59 session Intro (doc) in "Intro" = Pure +
    60   options [document_variants = "intro"]
    61   theories
    62   files
    63     "../prepare_document"
    64     "../pdfsetup.sty"
    65     "../iman.sty"
    66     "../extra.sty"
    67     "../ttbox.sty"
    68     "../manual.bib"
    69     "document/build"
    70     "document/root.tex"
    71 
    72 session IsarImplementation (doc) in "IsarImplementation" = "HOL-Proofs" +
    73   options [document_variants = "implementation"]
    74   theories
    75     Eq
    76     Integration
    77     Isar
    78     Local_Theory
    79     ML
    80     Prelim
    81     Proof
    82     Syntax
    83     Tactic
    84   theories [parallel_proofs = 0]
    85     Logic
    86   files
    87     "../prepare_document"
    88     "../pdfsetup.sty"
    89     "../iman.sty"
    90     "../extra.sty"
    91     "../isar.sty"
    92     "../ttbox.sty"
    93     "../underscore.sty"
    94     "../manual.bib"
    95     "document/build"
    96     "document/root.tex"
    97     "document/style.sty"
    98 
    99 session IsarRef (doc) in "IsarRef" = HOL +
   100   options [document_variants = "isar-ref", quick_and_dirty, thy_output_source]
   101   theories
   102     Preface
   103     Synopsis
   104     Framework
   105     First_Order_Logic
   106     Outer_Syntax
   107     Document_Preparation
   108     Spec
   109     Proof
   110     Inner_Syntax
   111     Misc
   112     Generic
   113     HOL_Specific
   114     Quick_Reference
   115     Symbols
   116     ML_Tactic
   117   files
   118     "../prepare_document"
   119     "../pdfsetup.sty"
   120     "../iman.sty"
   121     "../extra.sty"
   122     "../isar.sty"
   123     "../ttbox.sty"
   124     "../underscore.sty"
   125     "../manual.bib"
   126     "document/build"
   127     "document/isar-vm.eps"
   128     "document/isar-vm.pdf"
   129     "document/isar-vm.svg"
   130     "document/root.tex"
   131     "document/showsymbols"
   132     "document/style.sty"
   133 
   134 session LaTeXsugar (doc) in "LaTeXsugar" = HOL +
   135   options [document_variants = "sugar"]
   136   theories [document = ""]
   137     "~~/src/HOL/Library/LaTeXsugar"
   138     "~~/src/HOL/Library/OptionalSugar"
   139   theories Sugar
   140   files
   141     "../prepare_document"
   142     "../pdfsetup.sty"
   143     "document/build"
   144     "document/mathpartir.sty"
   145     "document/root.bib"
   146     "document/root.tex"
   147 
   148 session Locales (doc) in "Locales" = HOL +
   149   options [document_variants = "locales", pretty_margin = 65, skip_proofs = false]
   150   theories
   151     Examples1
   152     Examples2
   153     Examples3
   154   files
   155     "../prepare_document"
   156     "../pdfsetup.sty"
   157     "document/build"
   158     "document/root.tex"
   159 
   160 session Logics (doc) in "Logics" = Pure +
   161   options [document_variants = "logics"]
   162   theories
   163   files
   164     "../prepare_document"
   165     "../pdfsetup.sty"
   166     "../iman.sty"
   167     "../extra.sty"
   168     "../ttbox.sty"
   169     "../manual.bib"
   170     "document/CTT.tex"
   171     "document/HOL.tex"
   172     "document/LK.tex"
   173     "document/Sequents.tex"
   174     "document/build"
   175     "document/preface.tex"
   176     "document/root.tex"
   177     "document/syntax.tex"
   178 
   179 session "Logics-ZF" (doc) in "ZF" = ZF +
   180   options [document_variants = "logics-ZF", print_mode = "brackets",
   181     thy_output_source]
   182   theories
   183     IFOL_examples
   184     FOL_examples
   185     ZF_examples
   186     If
   187     ZF_Isar
   188   files
   189     "../prepare_document"
   190     "../pdfsetup.sty"
   191     "../isar.sty"
   192     "../ttbox.sty"
   193     "../manual.bib"
   194     "../Logics/document/syntax.tex"
   195     "document/build"
   196     "document/root.tex"
   197 
   198 session Main (doc) in "Main" = HOL +
   199   options [document_variants = "main"]
   200   theories Main_Doc
   201   files
   202     "../prepare_document"
   203     "../pdfsetup.sty"
   204     "document/build"
   205     "document/root.tex"
   206 
   207 session Nitpick (doc) in "Nitpick" = Pure +
   208   options [document_variants = "nitpick"]
   209   theories
   210   files
   211     "../prepare_document"
   212     "../pdfsetup.sty"
   213     "../iman.sty"
   214     "../manual.bib"
   215     "document/build"
   216     "document/root.tex"
   217 
   218 session ProgProve (doc) in "ProgProve" = HOL +
   219   options [document_variants = "prog-prove", show_question_marks = false]
   220   theories
   221     Basics
   222     Bool_nat_list
   223     MyList
   224     Types_and_funs
   225     Logic
   226     Isar
   227   files
   228     "../prepare_document"
   229     "../pdfsetup.sty"
   230     "document/bang.eps"
   231     "document/bang.pdf"
   232     "document/build"
   233     "document/intro-isabelle.tex"
   234     "document/mathpartir.sty"
   235     "document/prelude.tex"
   236     "document/root.bib"
   237     "document/root.tex"
   238     "document/svmono.cls"
   239 
   240 session Sledgehammer (doc) in "Sledgehammer" = Pure +
   241   options [document_variants = "sledgehammer"]
   242   theories
   243   files
   244     "../prepare_document"
   245     "../pdfsetup.sty"
   246     "../iman.sty"
   247     "../manual.bib"
   248     "document/build"
   249     "document/root.tex"
   250 
   251 session System (doc) in "System" = Pure +
   252   options [document_variants = "system", thy_output_source]
   253   theories
   254     Basics
   255     Interfaces
   256     Sessions
   257     Presentation
   258     Scala
   259     Misc
   260   files
   261     "../prepare_document"
   262     "../IsarRef/document/style.sty"
   263     "../pdfsetup.sty"
   264     "../iman.sty"
   265     "../extra.sty"
   266     "../isar.sty"
   267     "../ttbox.sty"
   268     "../underscore.sty"
   269     "../manual.bib"
   270     "document/browser_screenshot.eps"
   271     "document/browser_screenshot.png"
   272     "document/build"
   273     "document/root.tex"
   274 
   275 session Tutorial (doc) in "Tutorial" = HOL +
   276   options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
   277   theories [thy_output_indent = 5]
   278     "ToyList/ToyList"
   279     "Ifexpr/Ifexpr"
   280     "CodeGen/CodeGen"
   281     "Trie/Trie"
   282     "Datatype/ABexpr"
   283     "Datatype/unfoldnested"
   284     "Datatype/Nested"
   285     "Datatype/Fundata"
   286     "Fun/fun0"
   287     "Advanced/simp2"
   288     "CTL/PDL"
   289     "CTL/CTL"
   290     "CTL/CTLind"
   291     "Inductive/Even"
   292     "Inductive/Mutual"
   293     "Inductive/Star"
   294     "Inductive/AB"
   295     "Inductive/Advanced"
   296     "Misc/Tree"
   297     "Misc/Tree2"
   298     "Misc/Plus"
   299     "Misc/case_exprs"
   300     "Misc/fakenat"
   301     "Misc/natsum"
   302     "Misc/pairs2"
   303     "Misc/Option2"
   304     "Misc/types"
   305     "Misc/prime_def"
   306     "Misc/simp"
   307     "Misc/Itrev"
   308     "Misc/AdvancedInd"
   309     "Misc/appendix"
   310   theories
   311     "Protocol/NS_Public"
   312     "Documents/Documents"
   313   theories [document = ""]
   314     "Types/Setup"
   315   theories [pretty_margin = 64, thy_output_indent = 0]
   316     "Types/Numbers"
   317     "Types/Pairs"
   318     "Types/Records"
   319     "Types/Typedefs"
   320     "Types/Overloading"
   321     "Types/Axioms"
   322     "Rules/Basic"
   323     "Rules/Blast"
   324     "Rules/Force"
   325   theories [pretty_margin = 64, thy_output_indent = 5]
   326     "Rules/Primes"
   327     "Rules/Forward"
   328     "Rules/Tacticals"
   329     "Rules/find2"
   330     "Sets/Examples"
   331     "Sets/Functions"
   332     "Sets/Relations"
   333     "Sets/Recur"
   334   files
   335     "ToyList/ToyList1"
   336     "ToyList/ToyList2"
   337     "../pdfsetup.sty"
   338     "../ttbox.sty"
   339     "../manual.bib"
   340     "document/advanced0.tex"
   341     "document/appendix0.tex"
   342     "document/basics.tex"
   343     "document/build"
   344     "document/cl2emono-modified.sty"
   345     "document/ctl0.tex"
   346     "document/documents0.tex"
   347     "document/fp.tex"
   348     "document/inductive0.tex"
   349     "document/isa-index"
   350     "document/Isa-logics.eps"
   351     "document/Isa-logics.pdf"
   352     "document/numerics.tex"
   353     "document/pghead.eps"
   354     "document/pghead.pdf"
   355     "document/preface.tex"
   356     "document/protocol.tex"
   357     "document/root.tex"
   358     "document/rules.tex"
   359     "document/sets.tex"
   360     "document/tutorial.sty"
   361     "document/typedef.pdf"
   362     "document/typedef.ps"
   363     "document/types0.tex"
   364