Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
doc-src/ROOT
changeset 49531 c5d0f19ef7cb
parent 49524 4854ced3e9d7
child 49541 4372b7cb858d
equal deleted inserted replaced
49530:3e17f343deb5 49531:c5d0f19ef7cb 
     1 session Classes! (doc) in "Classes/Thy" = HOL +
 
     1 session Classes! (doc) in "Classes/Thy" = HOL +
 
     2   options [browser_info = false, document = false, document_dump = document, document_dump_only]
 
     2   options [browser_info = false, document = false,
 
       
     3     document_dump = document, document_dump_mode = "tex"]
 
     3   theories [document = false] Setup
 
     4   theories [document = false] Setup
 
     4   theories Classes
 
     5   theories Classes
 
     5 
     6 
     6 session Codegen! (doc) in "Codegen/Thy" = "HOL-Library" +
 
     7 session Codegen! (doc) in "Codegen/Thy" = "HOL-Library" +
 
     7   options [browser_info = false, document = false, document_dump = document, document_dump_only,
 
     8   options [browser_info = false, document = false,
 
       
     9     document_dump = document, document_dump_mode = "tex",
 
     8     print_mode = "no_brackets,iff"]
 
    10     print_mode = "no_brackets,iff"]
 
     9   theories [document = false] Setup
 
    11   theories [document = false] Setup
 
    10   theories
 
    12   theories
 
    11     Introduction
 
    13     Introduction
 
    12     Foundations
 
    14     Foundations
 
    15     Evaluation
 
    17     Evaluation
 
    16     Adaptation
 
    18     Adaptation
 
    17     Further
 
    19     Further
 
    18 
    20 
    19 session Functions! (doc) in "Functions/Thy" = HOL +
 
    21 session Functions! (doc) in "Functions/Thy" = HOL +
 
    20   options [browser_info = false, document = false, document_dump = document, document_dump_only]
 
    22   options [browser_info = false, document = false,
 
       
    23     document_dump = document, document_dump_mode = "tex"]
 
    21   theories Functions
 
    24   theories Functions
 
    22 
    25 
    23 session IsarImplementation! (doc) in "IsarImplementation/Thy" = HOL +
 
    26 session IsarImplementation! (doc) in "IsarImplementation/Thy" = HOL +
 
    24   options [browser_info = false, document = false, document_dump = document, document_dump_only]
 
    27   options [browser_info = false, document = false,
 
       
    28     document_dump = document, document_dump_mode = "tex"]
 
    25   theories
 
    29   theories
 
    26     Eq
 
    30     Eq
 
    27     Integration
 
    31     Integration
 
    28     Isar
 
    32     Isar
 
    29     Local_Theory
 
    33     Local_Theory
 
    33     Proof
 
    37     Proof
 
    34     Syntax
 
    38     Syntax
 
    35     Tactic
 
    39     Tactic
 
    36 
    40 
    37 session IsarRef (doc) in "IsarRef/Thy" = HOL +
 
    41 session IsarRef (doc) in "IsarRef/Thy" = HOL +
 
    38   options [browser_info = false, document = false, document_dump = document, document_dump_only,
 
    42   options [browser_info = false, document = false,
 
       
    43     document_dump = document, document_dump_mode = "tex",
 
    39     quick_and_dirty]
 
    44     quick_and_dirty]
 
    40   theories
 
    45   theories
 
    41     Preface
 
    46     Preface
 
    42     Synopsis
 
    47     Synopsis
 
    43     Framework
 
    48     Framework
 
    53     Quick_Reference
 
    58     Quick_Reference
 
    54     Symbols
 
    59     Symbols
 
    55     ML_Tactic
 
    60     ML_Tactic
 
    56 
    61 
    57 session IsarRef (doc) in "IsarRef/Thy" = HOLCF +
 
    62 session IsarRef (doc) in "IsarRef/Thy" = HOLCF +
 
    58   options [browser_info = false, document = false, document_dump = document, document_dump_only,
 
    63   options [browser_info = false, document = false,
 
       
    64     document_dump = document, document_dump_mode = "tex",
 
    59     quick_and_dirty]
 
    65     quick_and_dirty]
 
    60   theories HOLCF_Specific
 
    66   theories HOLCF_Specific
 
    61 
    67 
    62 session IsarRef (doc) in "IsarRef/Thy" = ZF +
 
    68 session IsarRef (doc) in "IsarRef/Thy" = ZF +
 
    63   options [browser_info = false, document = false, document_dump = document, document_dump_only,
 
    69   options [browser_info = false, document = false,
 
       
    70     document_dump = document, document_dump_mode = "tex",
 
    64     quick_and_dirty]
 
    71     quick_and_dirty]
 
    65   theories ZF_Specific
 
    72   theories ZF_Specific
 
    66 
    73 
    67 session LaTeXsugar! (doc) in "LaTeXsugar/Sugar" = HOL +
 
    74 session LaTeXsugar! (doc) in "LaTeXsugar/Sugar" = HOL +
 
    68   options [browser_info = false, document = false, document_dump = document, document_dump_only,
 
    75   options [browser_info = false, document = false,
 
       
    76     document_dump = document, document_dump_mode = "tex",
 
    69     threads = 1]  (* FIXME *)
 
    77     threads = 1]  (* FIXME *)
 
    70   theories [document_dump = ""]
 
    78   theories [document_dump = ""]
 
    71     "~~/src/HOL/Library/LaTeXsugar"
 
    79     "~~/src/HOL/Library/LaTeXsugar"
 
    72     "~~/src/HOL/Library/OptionalSugar"
 
    80     "~~/src/HOL/Library/OptionalSugar"
 
    73   theories Sugar
 
    81   theories Sugar
 
    74 
    82 
    75 session Locales! (doc) in "Locales/Locales" = HOL +
 
    83 session Locales! (doc) in "Locales/Locales" = HOL +
 
    76   options [browser_info = false, document = false, document_dump = document, document_dump_only]
 
    84   options [browser_info = false, document = false,
 
       
    85     document_dump = document, document_dump_mode = "tex"]
 
    77   theories
 
    86   theories
 
    78     Examples1
 
    87     Examples1
 
    79     Examples2
 
    88     Examples2
 
    80     Examples3
 
    89     Examples3
 
    81 
    90 
    82 session Main! (doc) in "Main/Docs" = HOL +
 
    91 session Main! (doc) in "Main/Docs" = HOL +
 
    83   options [browser_info = false, document = false, document_dump = document, document_dump_only]
 
    92   options [browser_info = false, document = false,
 
       
    93     document_dump = document, document_dump_mode = "tex"]
 
    84   theories Main_Doc
 
    94   theories Main_Doc
 
    85 
    95 
    86 session ProgProve! (doc) in "ProgProve/Thys" = HOL +
 
    96 session ProgProve! (doc) in "ProgProve/Thys" = HOL +
 
    87   options [browser_info = false, document = false, document_dump = document, document_dump_only,
 
    97   options [browser_info = false, document = false,
 
       
    98     document_dump = document, document_dump_mode = "tex",
 
    88     show_question_marks = false]
 
    99     show_question_marks = false]
 
    89   theories
 
   100   theories
 
    90     Basics
 
   101     Basics
 
    91     Bool_nat_list
 
   102     Bool_nat_list
 
    92     MyList
 
   103     MyList
 
    93     Types_and_funs
 
   104     Types_and_funs
 
    94     Logic
 
   105     Logic
 
    95     Isar
 
   106     Isar
 
    96 
   107 
    97 session System! (doc) in "System/Thy" = Pure +
 
   108 session System! (doc) in "System/Thy" = Pure +
 
    98   options [browser_info = false, document = false, document_dump = document, document_dump_only]
 
   109   options [browser_info = false, document = false,
 
       
   110     document_dump = document, document_dump_mode = "tex"]
 
    99   theories
 
   111   theories
 
   100     Basics
 
   112     Basics
 
   101     Interfaces
 
   113     Interfaces
 
   102     Scala
 
   114     Scala
 
   103     Presentation
 
   115     Presentation
 
   104     Misc
 
   116     Misc
 
   105 
   117 
   106 (* session Tutorial (doc) in "Tutorial" = HOL + FIXME *)
 
   118 (* session Tutorial (doc) in "Tutorial" = HOL + FIXME *)
 
   107 
   119 
   108 session examples (doc) in "ZF" = ZF +
 
   120 session examples (doc) in "ZF" = ZF +
 
   109   options [browser_info = false, document = false, document_dump = document, document_dump_only,
 
   121   options [browser_info = false, document = false,
 
       
   122     document_dump = document, document_dump_mode = "tex",
 
   110     print_mode = "brackets"]
 
   123     print_mode = "brackets"]
 
   111   theories
 
   124   theories
 
   112     IFOL_examples
 
   125     IFOL_examples
 
   113     FOL_examples
 
   126     FOL_examples
 
   114     ZF_examples
 
   127     ZF_examples
wneuper/isa