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