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