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