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