src/Doc/ROOT
author haftmann
Wed Feb 22 20:24:50 2017 +0100 (2017-02-22)
changeset 65041 2525e680f94f
parent 64514 27914a4f8c70
child 65569 3cb6f3281ef1
permissions -rw-r--r--
basic documentation for computations
     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     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 +
    48   options [document_variants = "corec"]
    49   theories [document = false] "../Datatypes/Setup"
    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 +
    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 +
   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   theories [document = ""]
   248     "~~/src/HOL/Library/LaTeXsugar"
   249     "~~/src/HOL/Library/OptionalSugar"
   250   theories Sugar
   251   document_files (in "..")
   252     "prepare_document"
   253     "pdfsetup.sty"
   254   document_files
   255     "build"
   256     "mathpartir.sty"
   257     "root.bib"
   258     "root.tex"
   259 
   260 session Locales (doc) in "Locales" = HOL +
   261   options [document_variants = "locales", thy_output_margin = 65, skip_proofs = false]
   262   theories
   263     Examples1
   264     Examples2
   265     Examples3
   266   document_files (in "..")
   267     "prepare_document"
   268     "pdfsetup.sty"
   269   document_files
   270     "build"
   271     "root.bib"
   272     "root.tex"
   273 
   274 session Logics (doc) in "Logics" = Pure +
   275   options [document_variants = "logics"]
   276   theories
   277   document_files (in "..")
   278     "prepare_document"
   279     "pdfsetup.sty"
   280     "iman.sty"
   281     "extra.sty"
   282     "ttbox.sty"
   283     "manual.bib"
   284   document_files
   285     "CTT.tex"
   286     "HOL.tex"
   287     "LK.tex"
   288     "Sequents.tex"
   289     "build"
   290     "preface.tex"
   291     "root.tex"
   292     "syntax.tex"
   293 
   294 session Logics_ZF (doc) in "Logics_ZF" = ZF +
   295   options [document_variants = "logics-ZF", print_mode = "brackets",
   296     thy_output_source]
   297   theories
   298     IFOL_examples
   299     FOL_examples
   300     ZF_examples
   301     If
   302     ZF_Isar
   303   document_files (in "..")
   304     "prepare_document"
   305     "pdfsetup.sty"
   306     "isar.sty"
   307     "ttbox.sty"
   308     "manual.bib"
   309   document_files (in "../Logics/document")
   310     "syntax.tex"
   311   document_files
   312     "FOL.tex"
   313     "ZF.tex"
   314     "build"
   315     "logics.sty"
   316     "root.tex"
   317 
   318 session Main (doc) in "Main" = HOL +
   319   options [document_variants = "main"]
   320   theories Main_Doc
   321   document_files (in "..")
   322     "prepare_document"
   323     "pdfsetup.sty"
   324   document_files
   325     "build"
   326     "root.tex"
   327 
   328 session Nitpick (doc) in "Nitpick" = Pure +
   329   options [document_variants = "nitpick"]
   330   theories
   331   document_files (in "..")
   332     "prepare_document"
   333     "pdfsetup.sty"
   334     "iman.sty"
   335     "manual.bib"
   336   document_files
   337     "build"
   338     "root.tex"
   339 
   340 session Prog_Prove (doc) in "Prog_Prove" = HOL +
   341   options [document_variants = "prog-prove", show_question_marks = false]
   342   theories
   343     Basics
   344     Bool_nat_list
   345     MyList
   346     Types_and_funs
   347     Logic
   348     Isar
   349   document_files (in ".")
   350     "MyList.thy"
   351   document_files (in "..")
   352     "prepare_document"
   353     "pdfsetup.sty"
   354   document_files
   355     "bang.pdf"
   356     "build"
   357     "intro-isabelle.tex"
   358     "mathpartir.sty"
   359     "prelude.tex"
   360     "root.bib"
   361     "root.tex"
   362     "svmono.cls"
   363 
   364 session Sledgehammer (doc) in "Sledgehammer" = Pure +
   365   options [document_variants = "sledgehammer"]
   366   theories
   367   document_files (in "..")
   368     "prepare_document"
   369     "pdfsetup.sty"
   370     "iman.sty"
   371     "manual.bib"
   372   document_files
   373     "build"
   374     "root.tex"
   375 
   376 session System (doc) in "System" = Pure +
   377   options [document_variants = "system", thy_output_source]
   378   theories
   379     Environment
   380     Sessions
   381     Presentation
   382     Scala
   383     Misc
   384   document_files (in "..")
   385     "prepare_document"
   386     "pdfsetup.sty"
   387     "iman.sty"
   388     "extra.sty"
   389     "isar.sty"
   390     "ttbox.sty"
   391     "underscore.sty"
   392     "manual.bib"
   393   document_files (in "../Isar_Ref/document")
   394     "style.sty"
   395   document_files
   396     "build"
   397     "root.tex"
   398 
   399 session Tutorial (doc) in "Tutorial" = HOL +
   400   options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
   401   theories [threads = 1]
   402     "ToyList/ToyList_Test"
   403   theories [thy_output_indent = 5]
   404     "ToyList/ToyList"
   405     "Ifexpr/Ifexpr"
   406     "CodeGen/CodeGen"
   407     "Trie/Trie"
   408     "Datatype/ABexpr"
   409     "Datatype/unfoldnested"
   410     "Datatype/Nested"
   411     "Datatype/Fundata"
   412     "Fun/fun0"
   413     "Advanced/simp2"
   414     "CTL/PDL"
   415     "CTL/CTL"
   416     "CTL/CTLind"
   417     "Inductive/Even"
   418     "Inductive/Mutual"
   419     "Inductive/Star"
   420     "Inductive/AB"
   421     "Inductive/Advanced"
   422     "Misc/Tree"
   423     "Misc/Tree2"
   424     "Misc/Plus"
   425     "Misc/case_exprs"
   426     "Misc/fakenat"
   427     "Misc/natsum"
   428     "Misc/pairs2"
   429     "Misc/Option2"
   430     "Misc/types"
   431     "Misc/prime_def"
   432     "Misc/simp"
   433     "Misc/Itrev"
   434     "Misc/AdvancedInd"
   435     "Misc/appendix"
   436   theories
   437     "Protocol/NS_Public"
   438     "Documents/Documents"
   439   theories [document = ""]
   440     "Types/Setup"
   441   theories [thy_output_margin = 64, thy_output_indent = 0]
   442     "Types/Numbers"
   443     "Types/Pairs"
   444     "Types/Records"
   445     "Types/Typedefs"
   446     "Types/Overloading"
   447     "Types/Axioms"
   448     "Rules/Basic"
   449     "Rules/Blast"
   450     "Rules/Force"
   451   theories [thy_output_margin = 64, thy_output_indent = 5]
   452     "Rules/TPrimes"
   453     "Rules/Forward"
   454     "Rules/Tacticals"
   455     "Rules/find2"
   456     "Sets/Examples"
   457     "Sets/Functions"
   458     "Sets/Relations"
   459     "Sets/Recur"
   460   document_files (in "ToyList")
   461     "ToyList1.txt"
   462     "ToyList2.txt"
   463   document_files (in "..")
   464     "pdfsetup.sty"
   465     "ttbox.sty"
   466     "manual.bib"
   467   document_files
   468     "advanced0.tex"
   469     "appendix0.tex"
   470     "basics.tex"
   471     "build"
   472     "cl2emono-modified.sty"
   473     "ctl0.tex"
   474     "documents0.tex"
   475     "fp.tex"
   476     "inductive0.tex"
   477     "isa-index"
   478     "Isa-logics.pdf"
   479     "numerics.tex"
   480     "pghead.pdf"
   481     "preface.tex"
   482     "protocol.tex"
   483     "root.tex"
   484     "rules.tex"
   485     "sets.tex"
   486     "tutorial.sty"
   487     "typedef.pdf"
   488     "types0.tex"
   489 
   490 session Typeclass_Hierarchy (doc) in "Typeclass_Hierarchy" = "Typeclass_Hierarchy_Basics" +
   491   options [document_variants = "typeclass_hierarchy"]
   492   theories Typeclass_Hierarchy
   493   document_files (in "..")
   494     "prepare_document"
   495     "pdfsetup.sty"
   496     "iman.sty"
   497     "extra.sty"
   498     "isar.sty"
   499     "manual.bib"
   500   document_files
   501     "build"
   502     "root.tex"
   503     "style.sty"
   504 
   505 session Typeclass_Hierarchy_Basics in "Typeclass_Hierarchy" = "HOL" +
   506   options [document = false]
   507   theories
   508     Setup