src/Doc/ROOT
author wenzelm
Mon Jul 06 11:14:44 2015 +0200 (2015-07-06)
changeset 60656 aabae0331b2f
parent 60484 98ee86354354
child 60674 2f66099fb472
permissions -rw-r--r--
removed outdated and mostly obsolete material;
     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-Proofs" +
   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     Misc
   170     Generic
   171     HOL_Specific
   172     Quick_Reference
   173     Symbols
   174   document_files (in "..")
   175     "prepare_document"
   176     "pdfsetup.sty"
   177     "iman.sty"
   178     "extra.sty"
   179     "isar.sty"
   180     "ttbox.sty"
   181     "underscore.sty"
   182     "manual.bib"
   183   document_files
   184     "build"
   185     "isar-vm.pdf"
   186     "isar-vm.svg"
   187     "root.tex"
   188     "showsymbols"
   189     "style.sty"
   190 
   191 session JEdit (doc) in "JEdit" = HOL +
   192   options [document_variants = "jedit", thy_output_source]
   193   theories
   194     JEdit
   195   document_files (in "..")
   196     "extra.sty"
   197     "iman.sty"
   198     "isar.sty"
   199     "manual.bib"
   200     "pdfsetup.sty"
   201     "prepare_document"
   202     "ttbox.sty"
   203     "underscore.sty"
   204   document_files (in "../Isar_Ref/document")
   205     "style.sty"
   206   document_files
   207     "auto-tools.png"
   208     "bibtex-mode.png"
   209     "build"
   210     "cite-completion.png"
   211     "isabelle-jedit.png"
   212     "isabelle-jedit-hdpi.png"
   213     "output.png"
   214     "query.png"
   215     "popup1.png"
   216     "popup2.png"
   217     "root.tex"
   218     "sidekick.png"
   219     "sidekick-document.png"
   220     "sledgehammer.png"
   221     "theories.png"
   222 
   223 session Sugar (doc) in "Sugar" = HOL +
   224   options [document_variants = "sugar"]
   225   theories [document = ""]
   226     "~~/src/HOL/Library/LaTeXsugar"
   227     "~~/src/HOL/Library/OptionalSugar"
   228   theories Sugar
   229   document_files (in "..")
   230     "prepare_document"
   231     "pdfsetup.sty"
   232   document_files
   233     "build"
   234     "mathpartir.sty"
   235     "root.bib"
   236     "root.tex"
   237 
   238 session Locales (doc) in "Locales" = HOL +
   239   options [document_variants = "locales", thy_output_margin = 65, skip_proofs = false]
   240   theories
   241     Examples1
   242     Examples2
   243     Examples3
   244   document_files (in "..")
   245     "prepare_document"
   246     "pdfsetup.sty"
   247   document_files
   248     "build"
   249     "root.bib"
   250     "root.tex"
   251 
   252 session Logics (doc) in "Logics" = Pure +
   253   options [document_variants = "logics"]
   254   theories
   255   document_files (in "..")
   256     "prepare_document"
   257     "pdfsetup.sty"
   258     "iman.sty"
   259     "extra.sty"
   260     "ttbox.sty"
   261     "manual.bib"
   262   document_files
   263     "CTT.tex"
   264     "HOL.tex"
   265     "LK.tex"
   266     "Sequents.tex"
   267     "build"
   268     "preface.tex"
   269     "root.tex"
   270     "syntax.tex"
   271 
   272 session Logics_ZF (doc) in "Logics_ZF" = ZF +
   273   options [document_variants = "logics-ZF", print_mode = "brackets",
   274     thy_output_source]
   275   theories
   276     IFOL_examples
   277     FOL_examples
   278     ZF_examples
   279     If
   280     ZF_Isar
   281   document_files (in "..")
   282     "prepare_document"
   283     "pdfsetup.sty"
   284     "isar.sty"
   285     "ttbox.sty"
   286     "manual.bib"
   287   document_files (in "../Logics/document")
   288     "syntax.tex"
   289   document_files
   290     "FOL.tex"
   291     "ZF.tex"
   292     "build"
   293     "logics.sty"
   294     "root.tex"
   295 
   296 session Main (doc) in "Main" = HOL +
   297   options [document_variants = "main"]
   298   theories Main_Doc
   299   document_files (in "..")
   300     "prepare_document"
   301     "pdfsetup.sty"
   302   document_files
   303     "build"
   304     "root.tex"
   305 
   306 session Nitpick (doc) in "Nitpick" = Pure +
   307   options [document_variants = "nitpick"]
   308   theories
   309   document_files (in "..")
   310     "prepare_document"
   311     "pdfsetup.sty"
   312     "iman.sty"
   313     "manual.bib"
   314   document_files
   315     "build"
   316     "root.tex"
   317 
   318 session Prog_Prove (doc) in "Prog_Prove" = HOL +
   319   options [document_variants = "prog-prove", show_question_marks = false]
   320   theories
   321     Basics
   322     Bool_nat_list
   323     MyList
   324     Types_and_funs
   325     Logic
   326     Isar
   327   document_files (in ".")
   328     "MyList.thy"
   329   document_files (in "..")
   330     "prepare_document"
   331     "pdfsetup.sty"
   332   document_files
   333     "bang.pdf"
   334     "build"
   335     "intro-isabelle.tex"
   336     "mathpartir.sty"
   337     "prelude.tex"
   338     "root.bib"
   339     "root.tex"
   340     "svmono.cls"
   341 
   342 session Sledgehammer (doc) in "Sledgehammer" = Pure +
   343   options [document_variants = "sledgehammer"]
   344   theories
   345   document_files (in "..")
   346     "prepare_document"
   347     "pdfsetup.sty"
   348     "iman.sty"
   349     "manual.bib"
   350   document_files
   351     "build"
   352     "root.tex"
   353 
   354 session System (doc) in "System" = Pure +
   355   options [document_variants = "system", thy_output_source]
   356   theories
   357     Basics
   358     Sessions
   359     Presentation
   360     Scala
   361     Misc
   362   document_files (in "..")
   363     "prepare_document"
   364     "pdfsetup.sty"
   365     "iman.sty"
   366     "extra.sty"
   367     "isar.sty"
   368     "ttbox.sty"
   369     "underscore.sty"
   370     "manual.bib"
   371   document_files (in "../Isar_Ref/document")
   372     "style.sty"
   373   document_files
   374     "browser_screenshot.png"
   375     "build"
   376     "root.tex"
   377 
   378 session Tutorial (doc) in "Tutorial" = HOL +
   379   options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
   380   theories [threads = 1]
   381     "ToyList/ToyList_Test"
   382   theories [thy_output_indent = 5]
   383     "ToyList/ToyList"
   384     "Ifexpr/Ifexpr"
   385     "CodeGen/CodeGen"
   386     "Trie/Trie"
   387     "Datatype/ABexpr"
   388     "Datatype/unfoldnested"
   389     "Datatype/Nested"
   390     "Datatype/Fundata"
   391     "Fun/fun0"
   392     "Advanced/simp2"
   393     "CTL/PDL"
   394     "CTL/CTL"
   395     "CTL/CTLind"
   396     "Inductive/Even"
   397     "Inductive/Mutual"
   398     "Inductive/Star"
   399     "Inductive/AB"
   400     "Inductive/Advanced"
   401     "Misc/Tree"
   402     "Misc/Tree2"
   403     "Misc/Plus"
   404     "Misc/case_exprs"
   405     "Misc/fakenat"
   406     "Misc/natsum"
   407     "Misc/pairs2"
   408     "Misc/Option2"
   409     "Misc/types"
   410     "Misc/prime_def"
   411     "Misc/simp"
   412     "Misc/Itrev"
   413     "Misc/AdvancedInd"
   414     "Misc/appendix"
   415   theories
   416     "Protocol/NS_Public"
   417     "Documents/Documents"
   418   theories [document = ""]
   419     "Types/Setup"
   420   theories [thy_output_margin = 64, thy_output_indent = 0]
   421     "Types/Numbers"
   422     "Types/Pairs"
   423     "Types/Records"
   424     "Types/Typedefs"
   425     "Types/Overloading"
   426     "Types/Axioms"
   427     "Rules/Basic"
   428     "Rules/Blast"
   429     "Rules/Force"
   430   theories [thy_output_margin = 64, thy_output_indent = 5]
   431     "Rules/TPrimes"
   432     "Rules/Forward"
   433     "Rules/Tacticals"
   434     "Rules/find2"
   435     "Sets/Examples"
   436     "Sets/Functions"
   437     "Sets/Relations"
   438     "Sets/Recur"
   439   document_files (in "ToyList")
   440     "ToyList1.txt"
   441     "ToyList2.txt"
   442   document_files (in "..")
   443     "pdfsetup.sty"
   444     "ttbox.sty"
   445     "manual.bib"
   446   document_files
   447     "advanced0.tex"
   448     "appendix0.tex"
   449     "basics.tex"
   450     "build"
   451     "cl2emono-modified.sty"
   452     "ctl0.tex"
   453     "documents0.tex"
   454     "fp.tex"
   455     "inductive0.tex"
   456     "isa-index"
   457     "Isa-logics.pdf"
   458     "numerics.tex"
   459     "pghead.pdf"
   460     "preface.tex"
   461     "protocol.tex"
   462     "root.tex"
   463     "rules.tex"
   464     "sets.tex"
   465     "tutorial.sty"
   466     "typedef.pdf"
   467     "types0.tex"