src/Doc/ROOT
author wenzelm
Wed Mar 27 18:04:21 2013 +0100 (2013-03-27)
changeset 51558 91f8bed6d0a4
parent 51397 03b586ee5930
child 52410 fb1fb867c146
permissions -rw-r--r--
allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
     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 +
    73   options [document_variants = "implementation"]
    74   theories
    75     Eq
    76     Integration
    77     Isar
    78     Local_Theory
    79     Logic
    80     ML
    81     Prelim
    82     Proof
    83     Syntax
    84     Tactic
    85   files
    86     "../prepare_document"
    87     "../pdfsetup.sty"
    88     "../iman.sty"
    89     "../extra.sty"
    90     "../isar.sty"
    91     "../ttbox.sty"
    92     "../underscore.sty"
    93     "../manual.bib"
    94     "document/build"
    95     "document/root.tex"
    96     "document/style.sty"
    97 
    98 session IsarRef (doc) in "IsarRef" = HOL +
    99   options [document_variants = "isar-ref", quick_and_dirty, thy_output_source]
   100   theories
   101     Preface
   102     Synopsis
   103     Framework
   104     First_Order_Logic
   105     Outer_Syntax
   106     Document_Preparation
   107     Spec
   108     Proof
   109     Inner_Syntax
   110     Misc
   111     Generic
   112     HOL_Specific
   113     Quick_Reference
   114     Symbols
   115     ML_Tactic
   116   files
   117     "../prepare_document"
   118     "../pdfsetup.sty"
   119     "../iman.sty"
   120     "../extra.sty"
   121     "../isar.sty"
   122     "../ttbox.sty"
   123     "../underscore.sty"
   124     "../manual.bib"
   125     "document/build"
   126     "document/isar-vm.eps"
   127     "document/isar-vm.pdf"
   128     "document/isar-vm.svg"
   129     "document/root.tex"
   130     "document/showsymbols"
   131     "document/style.sty"
   132 
   133 session LaTeXsugar (doc) in "LaTeXsugar" = HOL +
   134   options [document_variants = "sugar"]
   135   theories [document = ""]
   136     "~~/src/HOL/Library/LaTeXsugar"
   137     "~~/src/HOL/Library/OptionalSugar"
   138   theories Sugar
   139   files
   140     "../prepare_document"
   141     "../pdfsetup.sty"
   142     "document/build"
   143     "document/mathpartir.sty"
   144     "document/root.bib"
   145     "document/root.tex"
   146 
   147 session Locales (doc) in "Locales" = HOL +
   148   options [document_variants = "locales", pretty_margin = 65, skip_proofs = false]
   149   theories
   150     Examples1
   151     Examples2
   152     Examples3
   153   files
   154     "../prepare_document"
   155     "../pdfsetup.sty"
   156     "document/build"
   157     "document/root.tex"
   158 
   159 session Logics (doc) in "Logics" = Pure +
   160   options [document_variants = "logics"]
   161   theories
   162   files
   163     "../prepare_document"
   164     "../pdfsetup.sty"
   165     "../iman.sty"
   166     "../extra.sty"
   167     "../ttbox.sty"
   168     "../manual.bib"
   169     "document/build"
   170     "document/root.tex"
   171 
   172 session "Logics-HOL" (doc) in "HOL" = Pure +
   173   options [document_variants = "logics-HOL"]
   174   theories
   175   files
   176     "../prepare_document"
   177     "../pdfsetup.sty"
   178     "../iman.sty"
   179     "../extra.sty"
   180     "../ttbox.sty"
   181     "../manual.bib"
   182     "../Logics/document/syntax.tex"
   183     "document/build"
   184     "document/root.tex"
   185 
   186 session "Logics-ZF" (doc) in "ZF" = ZF +
   187   options [document_variants = "logics-ZF", print_mode = "brackets",
   188     thy_output_source]
   189   theories
   190     IFOL_examples
   191     FOL_examples
   192     ZF_examples
   193     If
   194     ZF_Isar
   195   files
   196     "../prepare_document"
   197     "../pdfsetup.sty"
   198     "../isar.sty"
   199     "../ttbox.sty"
   200     "../manual.bib"
   201     "../Logics/document/syntax.tex"
   202     "document/build"
   203     "document/root.tex"
   204 
   205 session Main (doc) in "Main" = HOL +
   206   options [document_variants = "main"]
   207   theories Main_Doc
   208   files
   209     "../prepare_document"
   210     "../pdfsetup.sty"
   211     "document/build"
   212     "document/root.tex"
   213 
   214 session Nitpick (doc) in "Nitpick" = Pure +
   215   options [document_variants = "nitpick"]
   216   theories
   217   files
   218     "../prepare_document"
   219     "../pdfsetup.sty"
   220     "../iman.sty"
   221     "../manual.bib"
   222     "document/build"
   223     "document/root.tex"
   224 
   225 session ProgProve (doc) in "ProgProve" = HOL +
   226   options [document_variants = "prog-prove", show_question_marks = false]
   227   theories
   228     Basics
   229     Bool_nat_list
   230     MyList
   231     Types_and_funs
   232     Logic
   233     Isar
   234   files
   235     "../prepare_document"
   236     "../pdfsetup.sty"
   237     "document/bang.eps"
   238     "document/bang.pdf"
   239     "document/build"
   240     "document/intro-isabelle.tex"
   241     "document/mathpartir.sty"
   242     "document/prelude.tex"
   243     "document/root.bib"
   244     "document/root.tex"
   245     "document/svmono.cls"
   246 
   247 session Ref (doc) in "Ref" = Pure +
   248   options [document_variants = "ref"]
   249   theories
   250   files
   251     "../prepare_document"
   252     "../pdfsetup.sty"
   253     "../iman.sty"
   254     "../extra.sty"
   255     "../ttbox.sty"
   256     "../manual.bib"
   257     "document/build"
   258     "document/root.tex"
   259     "document/syntax.tex"
   260     "document/thm.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