src/Doc/ROOT
author wenzelm
Mon Jun 17 21:23:49 2013 +0200 (2013-06-17)
changeset 52412 4cfa094da3cb
parent 52410 fb1fb867c146
child 52414 8429123bc58a
permissions -rw-r--r--
more on concrete syntax of proof terms;
     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 [proofs = 2, 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/build"
   171     "document/root.tex"
   172 
   173 session "Logics-HOL" (doc) in "HOL" = Pure +
   174   options [document_variants = "logics-HOL"]
   175   theories
   176   files
   177     "../prepare_document"
   178     "../pdfsetup.sty"
   179     "../iman.sty"
   180     "../extra.sty"
   181     "../ttbox.sty"
   182     "../manual.bib"
   183     "../Logics/document/syntax.tex"
   184     "document/build"
   185     "document/root.tex"
   186 
   187 session "Logics-ZF" (doc) in "ZF" = ZF +
   188   options [document_variants = "logics-ZF", print_mode = "brackets",
   189     thy_output_source]
   190   theories
   191     IFOL_examples
   192     FOL_examples
   193     ZF_examples
   194     If
   195     ZF_Isar
   196   files
   197     "../prepare_document"
   198     "../pdfsetup.sty"
   199     "../isar.sty"
   200     "../ttbox.sty"
   201     "../manual.bib"
   202     "../Logics/document/syntax.tex"
   203     "document/build"
   204     "document/root.tex"
   205 
   206 session Main (doc) in "Main" = HOL +
   207   options [document_variants = "main"]
   208   theories Main_Doc
   209   files
   210     "../prepare_document"
   211     "../pdfsetup.sty"
   212     "document/build"
   213     "document/root.tex"
   214 
   215 session Nitpick (doc) in "Nitpick" = Pure +
   216   options [document_variants = "nitpick"]
   217   theories
   218   files
   219     "../prepare_document"
   220     "../pdfsetup.sty"
   221     "../iman.sty"
   222     "../manual.bib"
   223     "document/build"
   224     "document/root.tex"
   225 
   226 session ProgProve (doc) in "ProgProve" = HOL +
   227   options [document_variants = "prog-prove", show_question_marks = false]
   228   theories
   229     Basics
   230     Bool_nat_list
   231     MyList
   232     Types_and_funs
   233     Logic
   234     Isar
   235   files
   236     "../prepare_document"
   237     "../pdfsetup.sty"
   238     "document/bang.eps"
   239     "document/bang.pdf"
   240     "document/build"
   241     "document/intro-isabelle.tex"
   242     "document/mathpartir.sty"
   243     "document/prelude.tex"
   244     "document/root.bib"
   245     "document/root.tex"
   246     "document/svmono.cls"
   247 
   248 session Ref (doc) in "Ref" = Pure +
   249   options [document_variants = "ref"]
   250   theories
   251   files
   252     "../prepare_document"
   253     "../pdfsetup.sty"
   254     "../iman.sty"
   255     "../extra.sty"
   256     "../ttbox.sty"
   257     "../manual.bib"
   258     "document/build"
   259     "document/root.tex"
   260     "document/syntax.tex"
   261 
   262 session Sledgehammer (doc) in "Sledgehammer" = Pure +
   263   options [document_variants = "sledgehammer"]
   264   theories
   265   files
   266     "../prepare_document"
   267     "../pdfsetup.sty"
   268     "../iman.sty"
   269     "../manual.bib"
   270     "document/build"
   271     "document/root.tex"
   272 
   273 session System (doc) in "System" = Pure +
   274   options [document_variants = "system", thy_output_source]
   275   theories
   276     Basics
   277     Interfaces
   278     Sessions
   279     Presentation
   280     Scala
   281     Misc
   282   files
   283     "../prepare_document"
   284     "../IsarRef/document/style.sty"
   285     "../pdfsetup.sty"
   286     "../iman.sty"
   287     "../extra.sty"
   288     "../isar.sty"
   289     "../ttbox.sty"
   290     "../underscore.sty"
   291     "../manual.bib"
   292     "document/browser_screenshot.eps"
   293     "document/browser_screenshot.png"
   294     "document/build"
   295     "document/root.tex"
   296 
   297 session Tutorial (doc) in "Tutorial" = HOL +
   298   options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
   299   theories [thy_output_indent = 5]
   300     "ToyList/ToyList"
   301     "Ifexpr/Ifexpr"
   302     "CodeGen/CodeGen"
   303     "Trie/Trie"
   304     "Datatype/ABexpr"
   305     "Datatype/unfoldnested"
   306     "Datatype/Nested"
   307     "Datatype/Fundata"
   308     "Fun/fun0"
   309     "Advanced/simp2"
   310     "CTL/PDL"
   311     "CTL/CTL"
   312     "CTL/CTLind"
   313     "Inductive/Even"
   314     "Inductive/Mutual"
   315     "Inductive/Star"
   316     "Inductive/AB"
   317     "Inductive/Advanced"
   318     "Misc/Tree"
   319     "Misc/Tree2"
   320     "Misc/Plus"
   321     "Misc/case_exprs"
   322     "Misc/fakenat"
   323     "Misc/natsum"
   324     "Misc/pairs2"
   325     "Misc/Option2"
   326     "Misc/types"
   327     "Misc/prime_def"
   328     "Misc/simp"
   329     "Misc/Itrev"
   330     "Misc/AdvancedInd"
   331     "Misc/appendix"
   332   theories
   333     "Protocol/NS_Public"
   334     "Documents/Documents"
   335   theories [document = ""]
   336     "Types/Setup"
   337   theories [pretty_margin = 64, thy_output_indent = 0]
   338     "Types/Numbers"
   339     "Types/Pairs"
   340     "Types/Records"
   341     "Types/Typedefs"
   342     "Types/Overloading"
   343     "Types/Axioms"
   344     "Rules/Basic"
   345     "Rules/Blast"
   346     "Rules/Force"
   347   theories [pretty_margin = 64, thy_output_indent = 5]
   348     "Rules/Primes"
   349     "Rules/Forward"
   350     "Rules/Tacticals"
   351     "Rules/find2"
   352     "Sets/Examples"
   353     "Sets/Functions"
   354     "Sets/Relations"
   355     "Sets/Recur"
   356   files
   357     "ToyList/ToyList1"
   358     "ToyList/ToyList2"
   359     "../pdfsetup.sty"
   360     "../ttbox.sty"
   361     "../manual.bib"
   362     "document/advanced0.tex"
   363     "document/appendix0.tex"
   364     "document/basics.tex"
   365     "document/build"
   366     "document/cl2emono-modified.sty"
   367     "document/ctl0.tex"
   368     "document/documents0.tex"
   369     "document/fp.tex"
   370     "document/inductive0.tex"
   371     "document/isa-index"
   372     "document/Isa-logics.eps"
   373     "document/Isa-logics.pdf"
   374     "document/numerics.tex"
   375     "document/pghead.eps"
   376     "document/pghead.pdf"
   377     "document/preface.tex"
   378     "document/protocol.tex"
   379     "document/root.tex"
   380     "document/rules.tex"
   381     "document/sets.tex"
   382     "document/tutorial.sty"
   383     "document/typedef.pdf"
   384     "document/typedef.ps"
   385     "document/types0.tex"
   386