src/Doc/ROOT
author wenzelm
Wed Mar 25 11:39:52 2015 +0100 (2015-03-25)
changeset 59809 87641097d0f3
parent 59405 4a0b34ef0563
child 60255 0466bd194d74
permissions -rw-r--r--
tuned signature;
     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 Functions (doc) in "Functions" = HOL +
    63   options [document_variants = "functions", skip_proofs = false, quick_and_dirty]
    64   theories Functions
    65   document_files (in "..")
    66     "prepare_document"
    67     "pdfsetup.sty"
    68     "iman.sty"
    69     "extra.sty"
    70     "isar.sty"
    71     "manual.bib"
    72   document_files
    73     "build"
    74     "conclusion.tex"
    75     "intro.tex"
    76     "mathpartir.sty"
    77     "root.tex"
    78     "style.sty"
    79 
    80 session How_to_Prove_it (* FIXME (doc) *) in "How_to_Prove_it" = HOL +
    81   options [document_variants = "how_to_prove_it", show_question_marks = false]
    82   theories
    83     How_to_Prove_it
    84   document_files
    85     "root.tex"
    86     "root.bib"
    87     "prelude.tex"
    88 
    89 session Intro (doc) in "Intro" = Pure +
    90   options [document_variants = "intro"]
    91   theories
    92   document_files (in "..")
    93     "prepare_document"
    94     "pdfsetup.sty"
    95     "iman.sty"
    96     "extra.sty"
    97     "ttbox.sty"
    98     "manual.bib"
    99   document_files
   100     "advanced.tex"
   101     "build"
   102     "foundations.tex"
   103     "getting.tex"
   104     "root.tex"
   105 
   106 session Implementation (doc) in "Implementation" = "HOL-Proofs" +
   107   options [document_variants = "implementation", quick_and_dirty]
   108   theories
   109     Eq
   110     Integration
   111     Isar
   112     Local_Theory
   113     ML
   114     Prelim
   115     Proof
   116     Syntax
   117     Tactic
   118   theories [parallel_proofs = 0]
   119     Logic
   120   document_files (in "..")
   121     "prepare_document"
   122     "pdfsetup.sty"
   123     "iman.sty"
   124     "extra.sty"
   125     "isar.sty"
   126     "ttbox.sty"
   127     "underscore.sty"
   128     "manual.bib"
   129   document_files
   130     "build"
   131     "root.tex"
   132     "style.sty"
   133 
   134 session Isar_Ref (doc) in "Isar_Ref" = HOL +
   135   options [document_variants = "isar-ref", quick_and_dirty, thy_output_source]
   136   theories
   137     Preface
   138     Synopsis
   139     Framework
   140     First_Order_Logic
   141     Outer_Syntax
   142     Document_Preparation
   143     Spec
   144     Proof
   145     Inner_Syntax
   146     Misc
   147     Generic
   148     HOL_Specific
   149     Quick_Reference
   150     Symbols
   151     ML_Tactic
   152   document_files (in "..")
   153     "prepare_document"
   154     "pdfsetup.sty"
   155     "iman.sty"
   156     "extra.sty"
   157     "isar.sty"
   158     "ttbox.sty"
   159     "underscore.sty"
   160     "manual.bib"
   161   document_files
   162     "build"
   163     "isar-vm.pdf"
   164     "isar-vm.svg"
   165     "root.tex"
   166     "showsymbols"
   167     "style.sty"
   168 
   169 session JEdit (doc) in "JEdit" = HOL +
   170   options [document_variants = "jedit", thy_output_source]
   171   theories
   172     JEdit
   173   document_files (in "..")
   174     "extra.sty"
   175     "iman.sty"
   176     "isar.sty"
   177     "manual.bib"
   178     "pdfsetup.sty"
   179     "prepare_document"
   180     "ttbox.sty"
   181     "underscore.sty"
   182   document_files (in "../Isar_Ref/document")
   183     "style.sty"
   184   document_files
   185     "auto-tools.png"
   186     "build"
   187     "isabelle-jedit.png"
   188     "output.png"
   189     "query.png"
   190     "popup1.png"
   191     "popup2.png"
   192     "root.tex"
   193     "sidekick.png"
   194     "sledgehammer.png"
   195     "theories.png"
   196 
   197 session Sugar (doc) in "Sugar" = HOL +
   198   options [document_variants = "sugar"]
   199   theories [document = ""]
   200     "~~/src/HOL/Library/LaTeXsugar"
   201     "~~/src/HOL/Library/OptionalSugar"
   202   theories Sugar
   203   document_files (in "..")
   204     "prepare_document"
   205     "pdfsetup.sty"
   206   document_files
   207     "build"
   208     "mathpartir.sty"
   209     "root.bib"
   210     "root.tex"
   211 
   212 session Locales (doc) in "Locales" = HOL +
   213   options [document_variants = "locales", thy_output_margin = 65, skip_proofs = false]
   214   theories
   215     Examples1
   216     Examples2
   217     Examples3
   218   document_files (in "..")
   219     "prepare_document"
   220     "pdfsetup.sty"
   221   document_files
   222     "build"
   223     "root.bib"
   224     "root.tex"
   225 
   226 session Logics (doc) in "Logics" = Pure +
   227   options [document_variants = "logics"]
   228   theories
   229   document_files (in "..")
   230     "prepare_document"
   231     "pdfsetup.sty"
   232     "iman.sty"
   233     "extra.sty"
   234     "ttbox.sty"
   235     "manual.bib"
   236   document_files
   237     "CTT.tex"
   238     "HOL.tex"
   239     "LK.tex"
   240     "Sequents.tex"
   241     "build"
   242     "preface.tex"
   243     "root.tex"
   244     "syntax.tex"
   245 
   246 session Logics_ZF (doc) in "Logics_ZF" = ZF +
   247   options [document_variants = "logics-ZF", print_mode = "brackets",
   248     thy_output_source]
   249   theories
   250     IFOL_examples
   251     FOL_examples
   252     ZF_examples
   253     If
   254     ZF_Isar
   255   document_files (in "..")
   256     "prepare_document"
   257     "pdfsetup.sty"
   258     "isar.sty"
   259     "ttbox.sty"
   260     "manual.bib"
   261   document_files (in "../Logics/document")
   262     "syntax.tex"
   263   document_files
   264     "FOL.tex"
   265     "ZF.tex"
   266     "build"
   267     "logics.sty"
   268     "root.tex"
   269 
   270 session Main (doc) in "Main" = HOL +
   271   options [document_variants = "main"]
   272   theories Main_Doc
   273   document_files (in "..")
   274     "prepare_document"
   275     "pdfsetup.sty"
   276   document_files
   277     "build"
   278     "root.tex"
   279 
   280 session Nitpick (doc) in "Nitpick" = Pure +
   281   options [document_variants = "nitpick"]
   282   theories
   283   document_files (in "..")
   284     "prepare_document"
   285     "pdfsetup.sty"
   286     "iman.sty"
   287     "manual.bib"
   288   document_files
   289     "build"
   290     "root.tex"
   291 
   292 session Prog_Prove (doc) in "Prog_Prove" = HOL +
   293   options [document_variants = "prog-prove", show_question_marks = false]
   294   theories
   295     Basics
   296     Bool_nat_list
   297     MyList
   298     Types_and_funs
   299     Logic
   300     Isar
   301   document_files (in ".")
   302     "MyList.thy"
   303   document_files (in "..")
   304     "prepare_document"
   305     "pdfsetup.sty"
   306   document_files
   307     "bang.pdf"
   308     "build"
   309     "intro-isabelle.tex"
   310     "mathpartir.sty"
   311     "prelude.tex"
   312     "root.bib"
   313     "root.tex"
   314     "svmono.cls"
   315 
   316 session Sledgehammer (doc) in "Sledgehammer" = Pure +
   317   options [document_variants = "sledgehammer"]
   318   theories
   319   document_files (in "..")
   320     "prepare_document"
   321     "pdfsetup.sty"
   322     "iman.sty"
   323     "manual.bib"
   324   document_files
   325     "build"
   326     "root.tex"
   327 
   328 session System (doc) in "System" = Pure +
   329   options [document_variants = "system", thy_output_source]
   330   theories
   331     Basics
   332     Sessions
   333     Presentation
   334     Scala
   335     Misc
   336   document_files (in "..")
   337     "prepare_document"
   338     "pdfsetup.sty"
   339     "iman.sty"
   340     "extra.sty"
   341     "isar.sty"
   342     "ttbox.sty"
   343     "underscore.sty"
   344     "manual.bib"
   345   document_files (in "../Isar_Ref/document")
   346     "style.sty"
   347   document_files
   348     "browser_screenshot.png"
   349     "build"
   350     "root.tex"
   351 
   352 session Tutorial (doc) in "Tutorial" = HOL +
   353   options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
   354   theories [threads = 1]
   355     "ToyList/ToyList_Test"
   356   theories [thy_output_indent = 5]
   357     "ToyList/ToyList"
   358     "Ifexpr/Ifexpr"
   359     "CodeGen/CodeGen"
   360     "Trie/Trie"
   361     "Datatype/ABexpr"
   362     "Datatype/unfoldnested"
   363     "Datatype/Nested"
   364     "Datatype/Fundata"
   365     "Fun/fun0"
   366     "Advanced/simp2"
   367     "CTL/PDL"
   368     "CTL/CTL"
   369     "CTL/CTLind"
   370     "Inductive/Even"
   371     "Inductive/Mutual"
   372     "Inductive/Star"
   373     "Inductive/AB"
   374     "Inductive/Advanced"
   375     "Misc/Tree"
   376     "Misc/Tree2"
   377     "Misc/Plus"
   378     "Misc/case_exprs"
   379     "Misc/fakenat"
   380     "Misc/natsum"
   381     "Misc/pairs2"
   382     "Misc/Option2"
   383     "Misc/types"
   384     "Misc/prime_def"
   385     "Misc/simp"
   386     "Misc/Itrev"
   387     "Misc/AdvancedInd"
   388     "Misc/appendix"
   389   theories
   390     "Protocol/NS_Public"
   391     "Documents/Documents"
   392   theories [document = ""]
   393     "Types/Setup"
   394   theories [thy_output_margin = 64, thy_output_indent = 0]
   395     "Types/Numbers"
   396     "Types/Pairs"
   397     "Types/Records"
   398     "Types/Typedefs"
   399     "Types/Overloading"
   400     "Types/Axioms"
   401     "Rules/Basic"
   402     "Rules/Blast"
   403     "Rules/Force"
   404   theories [thy_output_margin = 64, thy_output_indent = 5]
   405     "Rules/TPrimes"
   406     "Rules/Forward"
   407     "Rules/Tacticals"
   408     "Rules/find2"
   409     "Sets/Examples"
   410     "Sets/Functions"
   411     "Sets/Relations"
   412     "Sets/Recur"
   413   document_files (in "ToyList")
   414     "ToyList1.txt"
   415     "ToyList2.txt"
   416   document_files (in "..")
   417     "pdfsetup.sty"
   418     "ttbox.sty"
   419     "manual.bib"
   420   document_files
   421     "advanced0.tex"
   422     "appendix0.tex"
   423     "basics.tex"
   424     "build"
   425     "cl2emono-modified.sty"
   426     "ctl0.tex"
   427     "documents0.tex"
   428     "fp.tex"
   429     "inductive0.tex"
   430     "isa-index"
   431     "Isa-logics.pdf"
   432     "numerics.tex"
   433     "pghead.pdf"
   434     "preface.tex"
   435     "protocol.tex"
   436     "root.tex"
   437     "rules.tex"
   438     "sets.tex"
   439     "tutorial.sty"
   440     "typedef.pdf"
   441     "types0.tex"