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