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