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