src/Doc/ROOT
author wenzelm
Sat Sep 21 13:05:54 2013 +0200 (2013-09-21)
changeset 53769 036e80175bdd
parent 53618 4161d2b96b8c
child 54017 2a3c07f49615
permissions -rw-r--r--
basic setup for Isabelle/jEdit documentation;
     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]
    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" = Pure +
   147   options [document_variants = "jedit", thy_output_source]
   148   theories
   149     JEdit
   150   files
   151     "../prepare_document"
   152     "../IsarRef/document/style.sty"
   153     "../pdfsetup.sty"
   154     "../iman.sty"
   155     "../extra.sty"
   156     "../isar.sty"
   157     "../ttbox.sty"
   158     "../underscore.sty"
   159     "../manual.bib"
   160     "document/build"
   161     "document/root.tex"
   162 
   163 session LaTeXsugar (doc) in "LaTeXsugar" = HOL +
   164   options [document_variants = "sugar"]
   165   theories [document = ""]
   166     "~~/src/HOL/Library/LaTeXsugar"
   167     "~~/src/HOL/Library/OptionalSugar"
   168   theories Sugar
   169   files
   170     "../prepare_document"
   171     "../pdfsetup.sty"
   172     "document/build"
   173     "document/mathpartir.sty"
   174     "document/root.bib"
   175     "document/root.tex"
   176 
   177 session Locales (doc) in "Locales" = HOL +
   178   options [document_variants = "locales", pretty_margin = 65, skip_proofs = false]
   179   theories
   180     Examples1
   181     Examples2
   182     Examples3
   183   files
   184     "../prepare_document"
   185     "../pdfsetup.sty"
   186     "document/build"
   187     "document/root.tex"
   188 
   189 session Logics (doc) in "Logics" = Pure +
   190   options [document_variants = "logics"]
   191   theories
   192   files
   193     "../prepare_document"
   194     "../pdfsetup.sty"
   195     "../iman.sty"
   196     "../extra.sty"
   197     "../ttbox.sty"
   198     "../manual.bib"
   199     "document/CTT.tex"
   200     "document/HOL.tex"
   201     "document/LK.tex"
   202     "document/Sequents.tex"
   203     "document/build"
   204     "document/preface.tex"
   205     "document/root.tex"
   206     "document/syntax.tex"
   207 
   208 session "Logics-ZF" (doc) in "ZF" = ZF +
   209   options [document_variants = "logics-ZF", print_mode = "brackets",
   210     thy_output_source]
   211   theories
   212     IFOL_examples
   213     FOL_examples
   214     ZF_examples
   215     If
   216     ZF_Isar
   217   files
   218     "../prepare_document"
   219     "../pdfsetup.sty"
   220     "../isar.sty"
   221     "../ttbox.sty"
   222     "../manual.bib"
   223     "../Logics/document/syntax.tex"
   224     "document/build"
   225     "document/root.tex"
   226 
   227 session Main (doc) in "Main" = HOL +
   228   options [document_variants = "main"]
   229   theories Main_Doc
   230   files
   231     "../prepare_document"
   232     "../pdfsetup.sty"
   233     "document/build"
   234     "document/root.tex"
   235 
   236 session Nitpick (doc) in "Nitpick" = Pure +
   237   options [document_variants = "nitpick"]
   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 ProgProve (doc) in "ProgProve" = HOL +
   248   options [document_variants = "prog-prove", show_question_marks = false]
   249   theories
   250     Basics
   251     Bool_nat_list
   252     MyList
   253     Types_and_funs
   254     Logic
   255     Isar
   256   files
   257     "../prepare_document"
   258     "../pdfsetup.sty"
   259     "document/bang.pdf"
   260     "document/build"
   261     "document/intro-isabelle.tex"
   262     "document/mathpartir.sty"
   263     "document/prelude.tex"
   264     "document/root.bib"
   265     "document/root.tex"
   266     "document/svmono.cls"
   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.png"
   299     "document/build"
   300     "document/root.tex"
   301 
   302 session Tutorial (doc) in "Tutorial" = HOL +
   303   options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
   304   theories [threads = 1]
   305     "ToyList/ToyList_Test"
   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     "../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.pdf"
   380     "document/numerics.tex"
   381     "document/pghead.pdf"
   382     "document/preface.tex"
   383     "document/protocol.tex"
   384     "document/root.tex"
   385     "document/rules.tex"
   386     "document/sets.tex"
   387     "document/tutorial.sty"
   388     "document/typedef.pdf"
   389     "document/types0.tex"
   390