wneuper/isa: doc-src/ROOT@4372b7cb858d

     1 session Classes! (doc) in "Classes/Thy" = HOL +

     2   options [browser_info = false, document = false,

     3     document_dump = document, document_dump_mode = "tex"]

     4   theories [document = false] Setup

     5   theories Classes

     7 session Codegen! (doc) in "Codegen/Thy" = "HOL-Library" +

     8   options [browser_info = false, document = false,

     9     document_dump = document, document_dump_mode = "tex",

    10     print_mode = "no_brackets,iff"]

    11   theories [document = false] Setup

    12   theories

    13     Introduction

    14     Foundations

    15     Refinement

    16     Inductive_Predicate

    17     Evaluation

    18     Adaptation

    19     Further

    21 session Functions! (doc) in "Functions/Thy" = HOL +

    22   options [browser_info = false, document = false,

    23     document_dump = document, document_dump_mode = "tex"]

    24   theories Functions

    26 session IsarImplementation! (doc) in "IsarImplementation/Thy" = HOL +

    27   options [browser_info = false, document = false,

    28     document_dump = document, document_dump_mode = "tex"]

    29   theories

    30     Eq

    31     Integration

    32     Isar

    33     Local_Theory

    34     Logic

    35     ML

    36     Prelim

    37     Proof

    38     Syntax

    39     Tactic

    41 session IsarRef (doc) in "IsarRef/Thy" = HOL +

    42   options [browser_info = false, document = false,

    43     document_dump = document, document_dump_mode = "tex",

    44     quick_and_dirty]

    45   theories

    46     Preface

    47     Synopsis

    48     Framework

    49     First_Order_Logic

    50     Outer_Syntax

    51     Document_Preparation

    52     Spec

    53     Proof

    54     Inner_Syntax

    55     Misc

    56     Generic

    57     HOL_Specific

    58     Quick_Reference

    59     Symbols

    60     ML_Tactic

    62 session IsarRef (doc) in "IsarRef/Thy" = HOLCF +

    63   options [browser_info = false, document = false,

    64     document_dump = document, document_dump_mode = "tex",

    65     quick_and_dirty]

    66   theories HOLCF_Specific

    68 session IsarRef (doc) in "IsarRef/Thy" = ZF +

    69   options [browser_info = false, document = false,

    70     document_dump = document, document_dump_mode = "tex",

    71     quick_and_dirty]

    72   theories ZF_Specific

    74 session LaTeXsugar! (doc) in "LaTeXsugar/Sugar" = HOL +

    75   options [browser_info = false, document = false,

    76     document_dump = document, document_dump_mode = "tex",

    77     threads = 1]  (* FIXME *)

    78   theories [document_dump = ""]

    79     "~~/src/HOL/Library/LaTeXsugar"

    80     "~~/src/HOL/Library/OptionalSugar"

    81   theories Sugar

    83 session Locales! (doc) in "Locales/Locales" = HOL +

    84   options [browser_info = false, document = false,

    85     document_dump = document, document_dump_mode = "tex"]

    86   theories

    87     Examples1

    88     Examples2

    89     Examples3

    91 session Main! (doc) in "Main/Docs" = HOL +

    92   options [browser_info = false, document = false,

    93     document_dump = document, document_dump_mode = "tex"]

    94   theories Main_Doc

    96 session ProgProve! (doc) in "ProgProve/Thys" = HOL +

    97   options [browser_info = false, document = false,

    98     document_dump = document, document_dump_mode = "tex",

    99     show_question_marks = false]

   100   theories

   101     Basics

   102     Bool_nat_list

   103     MyList

   104     Types_and_funs

   105     Logic

   106     Isar

   108 session System! (doc) in "System/Thy" = Pure +

   109   options [browser_info = false, document = false,

   110     document_dump = document, document_dump_mode = "tex"]

   111   theories

   112     Basics

   113     Interfaces

   114     Scala

   115     Presentation

   116     Misc

   118 session Tutorial (doc) in "TutorialI" = HOL +

   119   options [browser_info = false, document = false,

   120     document_dump = document, document_dump_mode = "tex",

   121     print_mode = "brackets", threads = 1 (* FIXME *)]

   122   theories [thy_output_indent = 5]

   123     "ToyList/ToyList"

   124     "Ifexpr/Ifexpr"

   125     "CodeGen/CodeGen"

   126     "Trie/Trie"

   127     "Datatype/ABexpr"

   128     "Datatype/unfoldnested"

   129     "Datatype/Nested"

   130     "Datatype/Fundata"

   131     "Fun/fun0"

   132     "Advanced/simp2"

   133     "CTL/PDL"

   134     "CTL/CTL"

   135     "CTL/CTLind"

   136     "Inductive/Even"

   137     "Inductive/Mutual"

   138     "Inductive/Star"

   139     "Inductive/AB"

   140     "Inductive/Advanced"

   141     "Misc/Tree"

   142     "Misc/Tree2"

   143     "Misc/Plus"

   144     "Misc/case_exprs"

   145     "Misc/fakenat"

   146     "Misc/natsum"

   147     "Misc/pairs2"

   148     "Misc/Option2"

   149     "Misc/types"

   150     "Misc/prime_def"

   151     "Misc/simp"

   152     "Misc/Itrev"

   153     "Misc/AdvancedInd"

   154     "Misc/appendix"

   155   theories

   156     "Protocol/NS_Public"

   157     "Documents/Documents"

   158   theories [document_dump = ""]

   159     "Types/Setup"

   160   theories

   161     "Types/Numbers"

   162     "Types/Pairs"

   163     "Types/Records"

   164     "Types/Typedefs"

   165     "Types/Overloading"

   166     "Types/Axioms"

   167     "Rules/Basic"

   168     "Rules/Blast"

   169     "Rules/Force"

   170     "Rules/Forward"

   171     "Rules/Tacticals"

   172     "Rules/find2"

   173     "Sets/Examples"

   174     "Sets/Functions"

   175     "Sets/Relations"

   176     "Sets/Recur"

   178 session examples (doc) in "ZF" = ZF +

   179   options [browser_info = false, document = false,

   180     document_dump = document, document_dump_mode = "tex",

   181     print_mode = "brackets"]

   182   theories

   183     IFOL_examples

   184     FOL_examples

   185     ZF_examples

   186     If

author	wenzelm
	Thu, 26 Jul 2012 19:40:19 +0200
changeset 49541	4372b7cb858d
parent 49531	c5d0f19ef7cb
child 49593	21361b6189a6
permissions	-rw-r--r--