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