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