src/Doc/ROOT
author wenzelm
Mon Dec 22 16:44:24 2014 +0100 (2014-12-22)
changeset 59175 bf465f335e85
parent 58801 f420225a22d6
child 59378 065f349852e6
permissions -rw-r--r--
system option "pretty_margin" is superseded by "thy_output_margin";
     1 chapter Doc
     2 
     3 session Classes (doc) in "Classes" = HOL +
     4   options [document_variants = "classes", quick_and_dirty]
     5   theories [document = false] Setup
     6   theories Classes
     7   document_files (in "..")
     8     "prepare_document"
     9     "pdfsetup.sty"
    10     "iman.sty"
    11     "extra.sty"
    12     "isar.sty"
    13     "manual.bib"
    14   document_files
    15     "build"
    16     "root.tex"
    17     "style.sty"
    18 
    19 session Codegen (doc) in "Codegen" = "HOL-Library" +
    20   options [document_variants = "codegen", print_mode = "no_brackets,iff"]
    21   theories [document = false] Setup
    22   theories
    23     Introduction
    24     Foundations
    25     Refinement
    26     Inductive_Predicate
    27     Evaluation
    28     Adaptation
    29     Further
    30   document_files (in "..")
    31     "prepare_document"
    32     "pdfsetup.sty"
    33     "iman.sty"
    34     "extra.sty"
    35     "isar.sty"
    36     "manual.bib"
    37   document_files
    38     "build"
    39     "root.tex"
    40     "style.sty"
    41 
    42 session Datatypes (doc) in "Datatypes" = HOL +
    43   options [document_variants = "datatypes"]
    44   theories [document = false] Setup
    45   theories Datatypes
    46   document_files (in "..")
    47     "prepare_document"
    48     "pdfsetup.sty"
    49     "iman.sty"
    50     "extra.sty"
    51     "isar.sty"
    52     "manual.bib"
    53   document_files
    54     "build"
    55     "root.tex"
    56     "style.sty"
    57 
    58 session Functions (doc) in "Functions" = HOL +
    59   options [document_variants = "functions", skip_proofs = false, quick_and_dirty]
    60   theories Functions
    61   document_files (in "..")
    62     "prepare_document"
    63     "pdfsetup.sty"
    64     "iman.sty"
    65     "extra.sty"
    66     "isar.sty"
    67     "manual.bib"
    68   document_files
    69     "build"
    70     "conclusion.tex"
    71     "intro.tex"
    72     "mathpartir.sty"
    73     "root.tex"
    74     "style.sty"
    75 
    76 session How_to_Prove_it (* FIXME (doc) *) in "How_to_Prove_it" = HOL +
    77   options [document_variants = "how_to_prove_it", show_question_marks = false]
    78   theories
    79     How_to_Prove_it
    80   document_files
    81     "root.tex"
    82     "root.bib"
    83     "prelude.tex"
    84 
    85 session Intro (doc) in "Intro" = Pure +
    86   options [document_variants = "intro"]
    87   theories
    88   document_files (in "..")
    89     "prepare_document"
    90     "pdfsetup.sty"
    91     "iman.sty"
    92     "extra.sty"
    93     "ttbox.sty"
    94     "manual.bib"
    95   document_files
    96     "advanced.tex"
    97     "build"
    98     "foundations.tex"
    99     "getting.tex"
   100     "root.tex"
   101 
   102 session Implementation (doc) in "Implementation" = "HOL-Proofs" +
   103   options [document_variants = "implementation", quick_and_dirty]
   104   theories
   105     Eq
   106     Integration
   107     Isar
   108     Local_Theory
   109     ML
   110     Prelim
   111     Proof
   112     Syntax
   113     Tactic
   114   theories [parallel_proofs = 0]
   115     Logic
   116   document_files (in "..")
   117     "prepare_document"
   118     "pdfsetup.sty"
   119     "iman.sty"
   120     "extra.sty"
   121     "isar.sty"
   122     "ttbox.sty"
   123     "underscore.sty"
   124     "manual.bib"
   125   document_files
   126     "build"
   127     "root.tex"
   128     "style.sty"
   129 
   130 session Isar_Ref (doc) in "Isar_Ref" = HOL +
   131   options [document_variants = "isar-ref", quick_and_dirty, thy_output_source]
   132   theories
   133     Preface
   134     Synopsis
   135     Framework
   136     First_Order_Logic
   137     Outer_Syntax
   138     Document_Preparation
   139     Spec
   140     Proof
   141     Inner_Syntax
   142     Misc
   143     Generic
   144     HOL_Specific
   145     Quick_Reference
   146     Symbols
   147     ML_Tactic
   148   document_files (in "..")
   149     "prepare_document"
   150     "pdfsetup.sty"
   151     "iman.sty"
   152     "extra.sty"
   153     "isar.sty"
   154     "ttbox.sty"
   155     "underscore.sty"
   156     "manual.bib"
   157   document_files
   158     "build"
   159     "isar-vm.pdf"
   160     "isar-vm.svg"
   161     "root.tex"
   162     "showsymbols"
   163     "style.sty"
   164 
   165 session JEdit (doc) in "JEdit" = HOL +
   166   options [document_variants = "jedit", thy_output_source]
   167   theories
   168     JEdit
   169   document_files (in "..")
   170     "extra.sty"
   171     "iman.sty"
   172     "isar.sty"
   173     "manual.bib"
   174     "pdfsetup.sty"
   175     "prepare_document"
   176     "ttbox.sty"
   177     "underscore.sty"
   178   document_files (in "../Isar_Ref/document")
   179     "style.sty"
   180   document_files
   181     "auto-tools.png"
   182     "build"
   183     "isabelle-jedit.png"
   184     "output.png"
   185     "query.png"
   186     "popup1.png"
   187     "popup2.png"
   188     "root.tex"
   189     "sidekick.png"
   190     "sledgehammer.png"
   191     "theories.png"
   192 
   193 session Sugar (doc) in "Sugar" = HOL +
   194   options [document_variants = "sugar"]
   195   theories [document = ""]
   196     "~~/src/HOL/Library/LaTeXsugar"
   197     "~~/src/HOL/Library/OptionalSugar"
   198   theories Sugar
   199   document_files (in "..")
   200     "prepare_document"
   201     "pdfsetup.sty"
   202   document_files
   203     "build"
   204     "mathpartir.sty"
   205     "root.bib"
   206     "root.tex"
   207 
   208 session Locales (doc) in "Locales" = HOL +
   209   options [document_variants = "locales", thy_output_margin = 65, skip_proofs = false]
   210   theories
   211     Examples1
   212     Examples2
   213     Examples3
   214   document_files (in "..")
   215     "prepare_document"
   216     "pdfsetup.sty"
   217   document_files
   218     "build"
   219     "root.bib"
   220     "root.tex"
   221 
   222 session Logics (doc) in "Logics" = Pure +
   223   options [document_variants = "logics"]
   224   theories
   225   document_files (in "..")
   226     "prepare_document"
   227     "pdfsetup.sty"
   228     "iman.sty"
   229     "extra.sty"
   230     "ttbox.sty"
   231     "manual.bib"
   232   document_files
   233     "CTT.tex"
   234     "HOL.tex"
   235     "LK.tex"
   236     "Sequents.tex"
   237     "build"
   238     "preface.tex"
   239     "root.tex"
   240     "syntax.tex"
   241 
   242 session Logics_ZF (doc) in "Logics_ZF" = ZF +
   243   options [document_variants = "logics-ZF", print_mode = "brackets",
   244     thy_output_source]
   245   theories
   246     IFOL_examples
   247     FOL_examples
   248     ZF_examples
   249     If
   250     ZF_Isar
   251   document_files (in "..")
   252     "prepare_document"
   253     "pdfsetup.sty"
   254     "isar.sty"
   255     "ttbox.sty"
   256     "manual.bib"
   257   document_files (in "../Logics/document")
   258     "syntax.tex"
   259   document_files
   260     "FOL.tex"
   261     "ZF.tex"
   262     "build"
   263     "logics.sty"
   264     "root.tex"
   265 
   266 session Main (doc) in "Main" = HOL +
   267   options [document_variants = "main"]
   268   theories Main_Doc
   269   document_files (in "..")
   270     "prepare_document"
   271     "pdfsetup.sty"
   272   document_files
   273     "build"
   274     "root.tex"
   275 
   276 session Nitpick (doc) in "Nitpick" = Pure +
   277   options [document_variants = "nitpick"]
   278   theories
   279   document_files (in "..")
   280     "prepare_document"
   281     "pdfsetup.sty"
   282     "iman.sty"
   283     "manual.bib"
   284   document_files
   285     "build"
   286     "root.tex"
   287 
   288 session Prog_Prove (doc) in "Prog_Prove" = HOL +
   289   options [document_variants = "prog-prove", show_question_marks = false]
   290   theories
   291     Basics
   292     Bool_nat_list
   293     MyList
   294     Types_and_funs
   295     Logic
   296     Isar
   297   document_files (in ".")
   298     "MyList.thy"
   299   document_files (in "..")
   300     "prepare_document"
   301     "pdfsetup.sty"
   302   document_files
   303     "bang.pdf"
   304     "build"
   305     "intro-isabelle.tex"
   306     "mathpartir.sty"
   307     "prelude.tex"
   308     "root.bib"
   309     "root.tex"
   310     "svmono.cls"
   311 
   312 session Sledgehammer (doc) in "Sledgehammer" = Pure +
   313   options [document_variants = "sledgehammer"]
   314   theories
   315   document_files (in "..")
   316     "prepare_document"
   317     "pdfsetup.sty"
   318     "iman.sty"
   319     "manual.bib"
   320   document_files
   321     "build"
   322     "root.tex"
   323 
   324 session System (doc) in "System" = Pure +
   325   options [document_variants = "system", thy_output_source]
   326   theories
   327     Basics
   328     Sessions
   329     Presentation
   330     Scala
   331     Misc
   332   document_files (in "..")
   333     "prepare_document"
   334     "pdfsetup.sty"
   335     "iman.sty"
   336     "extra.sty"
   337     "isar.sty"
   338     "ttbox.sty"
   339     "underscore.sty"
   340     "manual.bib"
   341   document_files (in "../Isar_Ref/document")
   342     "style.sty"
   343   document_files
   344     "browser_screenshot.png"
   345     "build"
   346     "root.tex"
   347 
   348 session Tutorial (doc) in "Tutorial" = HOL +
   349   options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
   350   theories [threads = 1]
   351     "ToyList/ToyList_Test"
   352   theories [thy_output_indent = 5]
   353     "ToyList/ToyList"
   354     "Ifexpr/Ifexpr"
   355     "CodeGen/CodeGen"
   356     "Trie/Trie"
   357     "Datatype/ABexpr"
   358     "Datatype/unfoldnested"
   359     "Datatype/Nested"
   360     "Datatype/Fundata"
   361     "Fun/fun0"
   362     "Advanced/simp2"
   363     "CTL/PDL"
   364     "CTL/CTL"
   365     "CTL/CTLind"
   366     "Inductive/Even"
   367     "Inductive/Mutual"
   368     "Inductive/Star"
   369     "Inductive/AB"
   370     "Inductive/Advanced"
   371     "Misc/Tree"
   372     "Misc/Tree2"
   373     "Misc/Plus"
   374     "Misc/case_exprs"
   375     "Misc/fakenat"
   376     "Misc/natsum"
   377     "Misc/pairs2"
   378     "Misc/Option2"
   379     "Misc/types"
   380     "Misc/prime_def"
   381     "Misc/simp"
   382     "Misc/Itrev"
   383     "Misc/AdvancedInd"
   384     "Misc/appendix"
   385   theories
   386     "Protocol/NS_Public"
   387     "Documents/Documents"
   388   theories [document = ""]
   389     "Types/Setup"
   390   theories [thy_output_margin = 64, thy_output_indent = 0]
   391     "Types/Numbers"
   392     "Types/Pairs"
   393     "Types/Records"
   394     "Types/Typedefs"
   395     "Types/Overloading"
   396     "Types/Axioms"
   397     "Rules/Basic"
   398     "Rules/Blast"
   399     "Rules/Force"
   400   theories [thy_output_margin = 64, thy_output_indent = 5]
   401     "Rules/TPrimes"
   402     "Rules/Forward"
   403     "Rules/Tacticals"
   404     "Rules/find2"
   405     "Sets/Examples"
   406     "Sets/Functions"
   407     "Sets/Relations"
   408     "Sets/Recur"
   409   document_files (in "ToyList")
   410     "ToyList1.txt"
   411     "ToyList2.txt"
   412   document_files (in "..")
   413     "pdfsetup.sty"
   414     "ttbox.sty"
   415     "manual.bib"
   416   document_files
   417     "advanced0.tex"
   418     "appendix0.tex"
   419     "basics.tex"
   420     "build"
   421     "cl2emono-modified.sty"
   422     "ctl0.tex"
   423     "documents0.tex"
   424     "fp.tex"
   425     "inductive0.tex"
   426     "isa-index"
   427     "Isa-logics.pdf"
   428     "numerics.tex"
   429     "pghead.pdf"
   430     "preface.tex"
   431     "protocol.tex"
   432     "root.tex"
   433     "rules.tex"
   434     "sets.tex"
   435     "tutorial.sty"
   436     "typedef.pdf"
   437     "types0.tex"