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