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