src/Doc/ROOT
author wenzelm
Tue Aug 28 18:57:32 2012 +0200 (2012-08-28)
changeset 48985 5386df44a037
parent 48971 doc-src/ROOT@5a4bcf466156
child 49318 612a04e7c853
permissions -rw-r--r--
renamed doc-src to src/Doc;
renamed TutorialI to Tutorial;
     1 session Classes (doc) in "Classes" = HOL +
     2   options [document_variants = "classes"]
     3   theories [document = false] Setup
     4   theories Classes
     5   files
     6     "../prepare_document"
     7     "../pdfsetup.sty"
     8     "document/build"
     9     "document/root.tex"
    10     "document/style.sty"
    11 
    12 session Codegen (doc) in "Codegen" = "HOL-Library" +
    13   options [document_variants = "codegen", print_mode = "no_brackets,iff"]
    14   theories [document = false] Setup
    15   theories
    16     Introduction
    17     Foundations
    18     Refinement
    19     Inductive_Predicate
    20     Evaluation
    21     Adaptation
    22     Further
    23   files
    24     "../prepare_document"
    25     "../pdfsetup.sty"
    26     "document/adapt.tex"
    27     "document/architecture.tex"
    28     "document/build"
    29     "document/root.tex"
    30     "document/style.sty"
    31 
    32 session Functions (doc) in "Functions" = HOL +
    33   options [document_variants = "functions"]
    34   theories Functions
    35   files
    36     "../prepare_document"
    37     "../pdfsetup.sty"
    38     "../iman.sty"
    39     "../extra.sty"
    40     "../isar.sty"
    41     "../manual.bib"
    42     "document/build"
    43     "document/conclusion.tex"
    44     "document/intro.tex"
    45     "document/mathpartir.sty"
    46     "document/root.tex"
    47     "document/style.sty"
    48 
    49 session Intro (doc) in "Intro" = Pure +
    50   options [document_variants = "intro"]
    51   theories
    52   files
    53     "../prepare_document"
    54     "../pdfsetup.sty"
    55     "../iman.sty"
    56     "../extra.sty"
    57     "../ttbox.sty"
    58     "../proof.sty"
    59     "../manual.bib"
    60     "document/build"
    61     "document/root.tex"
    62 
    63 session IsarImplementation (doc) in "IsarImplementation" = HOL +
    64   options [document_variants = "implementation"]
    65   theories
    66     Eq
    67     Integration
    68     Isar
    69     Local_Theory
    70     Logic
    71     ML
    72     Prelim
    73     Proof
    74     Syntax
    75     Tactic
    76   files
    77     "../prepare_document"
    78     "../pdfsetup.sty"
    79     "../iman.sty"
    80     "../extra.sty"
    81     "../isar.sty"
    82     "../proof.sty"
    83     "../underscore.sty"
    84     "../ttbox.sty"
    85     "../manual.bib"
    86     "document/build"
    87     "document/root.tex"
    88     "document/style.sty"
    89 
    90 session IsarRef (doc) in "IsarRef" = HOL +
    91   options [document_variants = "isar-ref", quick_and_dirty, thy_output_source]
    92   theories
    93     Preface
    94     Synopsis
    95     Framework
    96     First_Order_Logic
    97     Outer_Syntax
    98     Document_Preparation
    99     Spec
   100     Proof
   101     Inner_Syntax
   102     Misc
   103     Generic
   104     HOL_Specific
   105     Quick_Reference
   106     Symbols
   107     ML_Tactic
   108   files
   109     "../prepare_document"
   110     "../pdfsetup.sty"
   111     "../iman.sty"
   112     "../extra.sty"
   113     "../ttbox.sty"
   114     "../proof.sty"
   115     "../isar.sty"
   116     "../manual.bib"
   117     "document/build"
   118     "document/isar-vm.eps"
   119     "document/isar-vm.pdf"
   120     "document/isar-vm.svg"
   121     "document/root.tex"
   122     "document/showsymbols"
   123     "document/style.sty"
   124 
   125 session LaTeXsugar (doc) in "LaTeXsugar" = HOL +
   126   options [document_variants = "sugar"]
   127   theories [document = ""]
   128     "~~/src/HOL/Library/LaTeXsugar"
   129     "~~/src/HOL/Library/OptionalSugar"
   130   theories Sugar
   131   files
   132     "../prepare_document"
   133     "../pdfsetup.sty"
   134     "document/build"
   135     "document/mathpartir.sty"
   136     "document/root.bib"
   137     "document/root.tex"
   138 
   139 session Locales (doc) in "Locales" = HOL +
   140   options [document_variants = "locales", pretty_margin = 65]
   141   theories
   142     Examples1
   143     Examples2
   144     Examples3
   145   files
   146     "../prepare_document"
   147     "../pdfsetup.sty"
   148     "document/build"
   149     "document/root.tex"
   150 
   151 session Logics (doc) in "Logics" = Pure +
   152   options [document_variants = "logics"]
   153   theories
   154   files
   155     "../prepare_document"
   156     "../pdfsetup.sty"
   157     "../iman.sty"
   158     "../extra.sty"
   159     "../ttbox.sty"
   160     "../proof.sty"
   161     "../manual.bib"
   162     "document/build"
   163     "document/root.tex"
   164 
   165 session "Logics-HOL" (doc) in "HOL" = Pure +
   166   options [document_variants = "logics-HOL"]
   167   theories
   168   files
   169     "../prepare_document"
   170     "../pdfsetup.sty"
   171     "../iman.sty"
   172     "../extra.sty"
   173     "../ttbox.sty"
   174     "../proof.sty"
   175     "../manual.bib"
   176     "../Logics/document/syntax.tex"
   177     "document/build"
   178     "document/root.tex"
   179 
   180 session "Logics-ZF" (doc) in "ZF" = ZF +
   181   options [document_variants = "logics-ZF", print_mode = "brackets",
   182     thy_output_source]
   183   theories
   184     IFOL_examples
   185     FOL_examples
   186     ZF_examples
   187     If
   188     ZF_Isar
   189   files
   190     "../prepare_document"
   191     "../pdfsetup.sty"
   192     "../isar.sty"
   193     "../ttbox.sty"
   194     "../proof.sty"
   195     "../manual.bib"
   196     "../Logics/document/syntax.tex"
   197     "document/build"
   198     "document/root.tex"
   199 
   200 session Main (doc) in "Main" = HOL +
   201   options [document_variants = "main"]
   202   theories Main_Doc
   203   files
   204     "../prepare_document"
   205     "../pdfsetup.sty"
   206     "document/build"
   207     "document/root.tex"
   208 
   209 session Nitpick (doc) in "Nitpick" = Pure +
   210   options [document_variants = "nitpick"]
   211   theories
   212   files
   213     "../prepare_document"
   214     "../pdfsetup.sty"
   215     "../iman.sty"
   216     "../manual.bib"
   217     "document/build"
   218     "document/root.tex"
   219 
   220 session ProgProve (doc) in "ProgProve" = HOL +
   221   options [document_variants = "prog-prove", show_question_marks = false]
   222   theories
   223     Basics
   224     Bool_nat_list
   225     MyList
   226     Types_and_funs
   227     Logic
   228     Isar
   229   files
   230     "../prepare_document"
   231     "../pdfsetup.sty"
   232     "document/bang.eps"
   233     "document/bang.pdf"
   234     "document/build"
   235     "document/intro-isabelle.tex"
   236     "document/mathpartir.sty"
   237     "document/prelude.tex"
   238     "document/root.bib"
   239     "document/root.tex"
   240     "document/svmono.cls"
   241 
   242 session Ref (doc) in "Ref" = Pure +
   243   options [document_variants = "ref"]
   244   theories
   245   files
   246     "../prepare_document"
   247     "../pdfsetup.sty"
   248     "../iman.sty"
   249     "../extra.sty"
   250     "../ttbox.sty"
   251     "../proof.sty"
   252     "../manual.bib"
   253     "document/build"
   254     "document/classical.tex"
   255     "document/root.tex"
   256     "document/simplifier.tex"
   257     "document/substitution.tex"
   258     "document/syntax.tex"
   259     "document/tactic.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     "../ttbox.sty"
   289     "../isar.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"]
   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     "../proof.sty"
   361     "../ttbox.sty"
   362     "../manual.bib"
   363     "document/advanced0.tex"
   364     "document/appendix0.tex"
   365     "document/basics.tex"
   366     "document/build"
   367     "document/cl2emono-modified.sty"
   368     "document/ctl0.tex"
   369     "document/documents0.tex"
   370     "document/fp.tex"
   371     "document/inductive0.tex"
   372     "document/isa-index"
   373     "document/Isa-logics.eps"
   374     "document/Isa-logics.pdf"
   375     "document/numerics.tex"
   376     "document/pghead.eps"
   377     "document/pghead.pdf"
   378     "document/preface.tex"
   379     "document/protocol.tex"
   380     "document/root.tex"
   381     "document/rules.tex"
   382     "document/sets.tex"
   383     "document/tutorial.sty"
   384     "document/typedef.pdf"
   385     "document/typedef.ps"
   386     "document/types0.tex"
   387