src/Doc/ROOT
author wenzelm
Sat Jul 27 21:21:47 2013 +0200 (2013-07-27)
changeset 52742 e7296939fec2
parent 52741 c08bd0a219f8
child 52792 3e651be14fcd
permissions -rw-r--r--
more direct inclusion of tikz pictures;
     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 Functions (doc) in "Functions" = HOL +
    41   options [document_variants = "functions", skip_proofs = false]
    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-Proofs" +
    71   options [document_variants = "implementation"]
    72   theories
    73     Eq
    74     Integration
    75     Isar
    76     Local_Theory
    77     ML
    78     Prelim
    79     Proof
    80     Syntax
    81     Tactic
    82   theories [parallel_proofs = 0]
    83     Logic
    84   files
    85     "../prepare_document"
    86     "../pdfsetup.sty"
    87     "../iman.sty"
    88     "../extra.sty"
    89     "../isar.sty"
    90     "../ttbox.sty"
    91     "../underscore.sty"
    92     "../manual.bib"
    93     "document/build"
    94     "document/root.tex"
    95     "document/style.sty"
    96 
    97 session IsarRef (doc) in "IsarRef" = HOL +
    98   options [document_variants = "isar-ref", quick_and_dirty, thy_output_source]
    99   theories
   100     Preface
   101     Synopsis
   102     Framework
   103     First_Order_Logic
   104     Outer_Syntax
   105     Document_Preparation
   106     Spec
   107     Proof
   108     Inner_Syntax
   109     Misc
   110     Generic
   111     HOL_Specific
   112     Quick_Reference
   113     Symbols
   114     ML_Tactic
   115   files
   116     "../prepare_document"
   117     "../pdfsetup.sty"
   118     "../iman.sty"
   119     "../extra.sty"
   120     "../isar.sty"
   121     "../ttbox.sty"
   122     "../underscore.sty"
   123     "../manual.bib"
   124     "document/build"
   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, skip_proofs = false]
   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/CTT.tex"
   168     "document/HOL.tex"
   169     "document/LK.tex"
   170     "document/Sequents.tex"
   171     "document/build"
   172     "document/preface.tex"
   173     "document/root.tex"
   174     "document/syntax.tex"
   175 
   176 session "Logics-ZF" (doc) in "ZF" = ZF +
   177   options [document_variants = "logics-ZF", print_mode = "brackets",
   178     thy_output_source]
   179   theories
   180     IFOL_examples
   181     FOL_examples
   182     ZF_examples
   183     If
   184     ZF_Isar
   185   files
   186     "../prepare_document"
   187     "../pdfsetup.sty"
   188     "../isar.sty"
   189     "../ttbox.sty"
   190     "../manual.bib"
   191     "../Logics/document/syntax.tex"
   192     "document/build"
   193     "document/root.tex"
   194 
   195 session Main (doc) in "Main" = HOL +
   196   options [document_variants = "main"]
   197   theories Main_Doc
   198   files
   199     "../prepare_document"
   200     "../pdfsetup.sty"
   201     "document/build"
   202     "document/root.tex"
   203 
   204 session Nitpick (doc) in "Nitpick" = Pure +
   205   options [document_variants = "nitpick"]
   206   theories
   207   files
   208     "../prepare_document"
   209     "../pdfsetup.sty"
   210     "../iman.sty"
   211     "../manual.bib"
   212     "document/build"
   213     "document/root.tex"
   214 
   215 session ProgProve (doc) in "ProgProve" = HOL +
   216   options [document_variants = "prog-prove", show_question_marks = false]
   217   theories
   218     Basics
   219     Bool_nat_list
   220     MyList
   221     Types_and_funs
   222     Logic
   223     Isar
   224   files
   225     "../prepare_document"
   226     "../pdfsetup.sty"
   227     "document/bang.pdf"
   228     "document/build"
   229     "document/intro-isabelle.tex"
   230     "document/mathpartir.sty"
   231     "document/prelude.tex"
   232     "document/root.bib"
   233     "document/root.tex"
   234     "document/svmono.cls"
   235 
   236 session Sledgehammer (doc) in "Sledgehammer" = Pure +
   237   options [document_variants = "sledgehammer"]
   238   theories
   239   files
   240     "../prepare_document"
   241     "../pdfsetup.sty"
   242     "../iman.sty"
   243     "../manual.bib"
   244     "document/build"
   245     "document/root.tex"
   246 
   247 session System (doc) in "System" = Pure +
   248   options [document_variants = "system", thy_output_source]
   249   theories
   250     Basics
   251     Interfaces
   252     Sessions
   253     Presentation
   254     Scala
   255     Misc
   256   files
   257     "../prepare_document"
   258     "../IsarRef/document/style.sty"
   259     "../pdfsetup.sty"
   260     "../iman.sty"
   261     "../extra.sty"
   262     "../isar.sty"
   263     "../ttbox.sty"
   264     "../underscore.sty"
   265     "../manual.bib"
   266     "document/browser_screenshot.png"
   267     "document/build"
   268     "document/root.tex"
   269 
   270 session Tutorial (doc) in "Tutorial" = HOL +
   271   options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
   272   theories [thy_output_indent = 5]
   273     "ToyList/ToyList"
   274     "Ifexpr/Ifexpr"
   275     "CodeGen/CodeGen"
   276     "Trie/Trie"
   277     "Datatype/ABexpr"
   278     "Datatype/unfoldnested"
   279     "Datatype/Nested"
   280     "Datatype/Fundata"
   281     "Fun/fun0"
   282     "Advanced/simp2"
   283     "CTL/PDL"
   284     "CTL/CTL"
   285     "CTL/CTLind"
   286     "Inductive/Even"
   287     "Inductive/Mutual"
   288     "Inductive/Star"
   289     "Inductive/AB"
   290     "Inductive/Advanced"
   291     "Misc/Tree"
   292     "Misc/Tree2"
   293     "Misc/Plus"
   294     "Misc/case_exprs"
   295     "Misc/fakenat"
   296     "Misc/natsum"
   297     "Misc/pairs2"
   298     "Misc/Option2"
   299     "Misc/types"
   300     "Misc/prime_def"
   301     "Misc/simp"
   302     "Misc/Itrev"
   303     "Misc/AdvancedInd"
   304     "Misc/appendix"
   305   theories
   306     "Protocol/NS_Public"
   307     "Documents/Documents"
   308   theories [document = ""]
   309     "Types/Setup"
   310   theories [pretty_margin = 64, thy_output_indent = 0]
   311     "Types/Numbers"
   312     "Types/Pairs"
   313     "Types/Records"
   314     "Types/Typedefs"
   315     "Types/Overloading"
   316     "Types/Axioms"
   317     "Rules/Basic"
   318     "Rules/Blast"
   319     "Rules/Force"
   320   theories [pretty_margin = 64, thy_output_indent = 5]
   321     "Rules/Primes"
   322     "Rules/Forward"
   323     "Rules/Tacticals"
   324     "Rules/find2"
   325     "Sets/Examples"
   326     "Sets/Functions"
   327     "Sets/Relations"
   328     "Sets/Recur"
   329   files
   330     "ToyList/ToyList1"
   331     "ToyList/ToyList2"
   332     "../pdfsetup.sty"
   333     "../ttbox.sty"
   334     "../manual.bib"
   335     "document/advanced0.tex"
   336     "document/appendix0.tex"
   337     "document/basics.tex"
   338     "document/build"
   339     "document/cl2emono-modified.sty"
   340     "document/ctl0.tex"
   341     "document/documents0.tex"
   342     "document/fp.tex"
   343     "document/inductive0.tex"
   344     "document/isa-index"
   345     "document/Isa-logics.pdf"
   346     "document/numerics.tex"
   347     "document/pghead.pdf"
   348     "document/preface.tex"
   349     "document/protocol.tex"
   350     "document/root.tex"
   351     "document/rules.tex"
   352     "document/sets.tex"
   353     "document/tutorial.sty"
   354     "document/typedef.pdf"
   355     "document/types0.tex"
   356