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