src/Doc/ROOT
author wenzelm
Sun Nov 11 16:19:55 2012 +0100 (2012-11-11)
changeset 50080 200f749c96db
parent 50074 0b02aaf7c7c5
child 50084 3a3c54342e58
permissions -rw-r--r--
updated section on ordered rewriting;
     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/substitution.tex"
   266     "document/syntax.tex"
   267     "document/thm.tex"
   268 
   269 session Sledgehammer (doc) in "Sledgehammer" = Pure +
   270   options [document_variants = "sledgehammer"]
   271   theories
   272   files
   273     "../prepare_document"
   274     "../pdfsetup.sty"
   275     "../iman.sty"
   276     "../manual.bib"
   277     "document/build"
   278     "document/root.tex"
   279 
   280 session System (doc) in "System" = Pure +
   281   options [document_variants = "system", thy_output_source]
   282   theories
   283     Basics
   284     Interfaces
   285     Sessions
   286     Presentation
   287     Scala
   288     Misc
   289   files
   290     "../prepare_document"
   291     "../IsarRef/document/style.sty"
   292     "../pdfsetup.sty"
   293     "../iman.sty"
   294     "../extra.sty"
   295     "../isar.sty"
   296     "../ttbox.sty"
   297     "../underscore.sty"
   298     "../manual.bib"
   299     "document/browser_screenshot.eps"
   300     "document/browser_screenshot.png"
   301     "document/build"
   302     "document/root.tex"
   303 
   304 session Tutorial (doc) in "Tutorial" = HOL +
   305   options [document_variants = "tutorial", print_mode = "brackets"]
   306   theories [thy_output_indent = 5]
   307     "ToyList/ToyList"
   308     "Ifexpr/Ifexpr"
   309     "CodeGen/CodeGen"
   310     "Trie/Trie"
   311     "Datatype/ABexpr"
   312     "Datatype/unfoldnested"
   313     "Datatype/Nested"
   314     "Datatype/Fundata"
   315     "Fun/fun0"
   316     "Advanced/simp2"
   317     "CTL/PDL"
   318     "CTL/CTL"
   319     "CTL/CTLind"
   320     "Inductive/Even"
   321     "Inductive/Mutual"
   322     "Inductive/Star"
   323     "Inductive/AB"
   324     "Inductive/Advanced"
   325     "Misc/Tree"
   326     "Misc/Tree2"
   327     "Misc/Plus"
   328     "Misc/case_exprs"
   329     "Misc/fakenat"
   330     "Misc/natsum"
   331     "Misc/pairs2"
   332     "Misc/Option2"
   333     "Misc/types"
   334     "Misc/prime_def"
   335     "Misc/simp"
   336     "Misc/Itrev"
   337     "Misc/AdvancedInd"
   338     "Misc/appendix"
   339   theories
   340     "Protocol/NS_Public"
   341     "Documents/Documents"
   342   theories [document = ""]
   343     "Types/Setup"
   344   theories [pretty_margin = 64, thy_output_indent = 0]
   345     "Types/Numbers"
   346     "Types/Pairs"
   347     "Types/Records"
   348     "Types/Typedefs"
   349     "Types/Overloading"
   350     "Types/Axioms"
   351     "Rules/Basic"
   352     "Rules/Blast"
   353     "Rules/Force"
   354   theories [pretty_margin = 64, thy_output_indent = 5]
   355     "Rules/Primes"
   356     "Rules/Forward"
   357     "Rules/Tacticals"
   358     "Rules/find2"
   359     "Sets/Examples"
   360     "Sets/Functions"
   361     "Sets/Relations"
   362     "Sets/Recur"
   363   files
   364     "ToyList/ToyList1"
   365     "ToyList/ToyList2"
   366     "../pdfsetup.sty"
   367     "../proof.sty"
   368     "../ttbox.sty"
   369     "../manual.bib"
   370     "document/advanced0.tex"
   371     "document/appendix0.tex"
   372     "document/basics.tex"
   373     "document/build"
   374     "document/cl2emono-modified.sty"
   375     "document/ctl0.tex"
   376     "document/documents0.tex"
   377     "document/fp.tex"
   378     "document/inductive0.tex"
   379     "document/isa-index"
   380     "document/Isa-logics.eps"
   381     "document/Isa-logics.pdf"
   382     "document/numerics.tex"
   383     "document/pghead.eps"
   384     "document/pghead.pdf"
   385     "document/preface.tex"
   386     "document/protocol.tex"
   387     "document/root.tex"
   388     "document/rules.tex"
   389     "document/sets.tex"
   390     "document/tutorial.sty"
   391     "document/typedef.pdf"
   392     "document/typedef.ps"
   393     "document/types0.tex"
   394