src/Pure/ROOT
author wenzelm
Fri Jul 12 11:07:02 2013 +0200 (2013-07-12)
changeset 52605 a2a805549c74
parent 52596 40298d383463
child 52711 155f02cacb2d
permissions -rw-r--r--
clarified module name;
wenzelm@51397
     1
chapter Pure
wenzelm@51397
     2
wenzelm@48738
     3
session RAW =
wenzelm@48916
     4
  theories
wenzelm@48347
     5
  files
wenzelm@48347
     6
    "General/exn.ML"
wenzelm@48347
     7
    "ML-Systems/compiler_polyml.ML"
wenzelm@48347
     8
    "ML-Systems/ml_name_space.ML"
wenzelm@48347
     9
    "ML-Systems/ml_pretty.ML"
wenzelm@48347
    10
    "ML-Systems/ml_system.ML"
wenzelm@48347
    11
    "ML-Systems/multithreading.ML"
wenzelm@48347
    12
    "ML-Systems/multithreading_polyml.ML"
wenzelm@48347
    13
    "ML-Systems/overloading_smlnj.ML"
wenzelm@48347
    14
    "ML-Systems/polyml.ML"
wenzelm@48347
    15
    "ML-Systems/pp_dummy.ML"
wenzelm@48347
    16
    "ML-Systems/proper_int.ML"
wenzelm@48347
    17
    "ML-Systems/single_assignment.ML"
wenzelm@48347
    18
    "ML-Systems/single_assignment_polyml.ML"
wenzelm@48347
    19
    "ML-Systems/smlnj.ML"
wenzelm@48347
    20
    "ML-Systems/thread_dummy.ML"
wenzelm@48347
    21
    "ML-Systems/universal.ML"
wenzelm@48347
    22
    "ML-Systems/unsynchronized.ML"
wenzelm@48347
    23
    "ML-Systems/use_context.ML"
wenzelm@48347
    24
wenzelm@48738
    25
session Pure =
wenzelm@48422
    26
  theories Pure
wenzelm@48514
    27
  files
wenzelm@48514
    28
    "General/exn.ML"
wenzelm@48514
    29
    "ML-Systems/compiler_polyml.ML"
wenzelm@48514
    30
    "ML-Systems/ml_name_space.ML"
wenzelm@48514
    31
    "ML-Systems/ml_pretty.ML"
wenzelm@48514
    32
    "ML-Systems/ml_system.ML"
wenzelm@48514
    33
    "ML-Systems/multithreading.ML"
wenzelm@48514
    34
    "ML-Systems/multithreading_polyml.ML"
wenzelm@48514
    35
    "ML-Systems/overloading_smlnj.ML"
wenzelm@48514
    36
    "ML-Systems/polyml.ML"
wenzelm@48514
    37
    "ML-Systems/pp_dummy.ML"
wenzelm@48514
    38
    "ML-Systems/proper_int.ML"
wenzelm@48514
    39
    "ML-Systems/single_assignment.ML"
wenzelm@48514
    40
    "ML-Systems/single_assignment_polyml.ML"
wenzelm@48514
    41
    "ML-Systems/smlnj.ML"
wenzelm@48514
    42
    "ML-Systems/thread_dummy.ML"
wenzelm@48514
    43
    "ML-Systems/universal.ML"
wenzelm@48514
    44
    "ML-Systems/unsynchronized.ML"
wenzelm@48514
    45
    "ML-Systems/use_context.ML"
wenzelm@48347
    46
wenzelm@48514
    47
    "Concurrent/bash.ML"
wenzelm@48514
    48
    "Concurrent/bash_sequential.ML"
wenzelm@48514
    49
    "Concurrent/cache.ML"
wenzelm@52050
    50
    "Concurrent/event_timer.ML"
wenzelm@48514
    51
    "Concurrent/future.ML"
wenzelm@48514
    52
    "Concurrent/lazy.ML"
wenzelm@48514
    53
    "Concurrent/lazy_sequential.ML"
wenzelm@48514
    54
    "Concurrent/mailbox.ML"
wenzelm@48514
    55
    "Concurrent/par_exn.ML"
wenzelm@48514
    56
    "Concurrent/par_list.ML"
wenzelm@48514
    57
    "Concurrent/par_list_sequential.ML"
wenzelm@48514
    58
    "Concurrent/simple_thread.ML"
wenzelm@48514
    59
    "Concurrent/single_assignment.ML"
wenzelm@48514
    60
    "Concurrent/single_assignment_sequential.ML"
wenzelm@48514
    61
    "Concurrent/synchronized.ML"
wenzelm@48514
    62
    "Concurrent/synchronized_sequential.ML"
wenzelm@48514
    63
    "Concurrent/task_queue.ML"
wenzelm@48514
    64
    "Concurrent/time_limit.ML"
wenzelm@48514
    65
    "General/alist.ML"
wenzelm@48514
    66
    "General/antiquote.ML"
wenzelm@48514
    67
    "General/balanced_tree.ML"
wenzelm@48514
    68
    "General/basics.ML"
wenzelm@48514
    69
    "General/binding.ML"
wenzelm@48514
    70
    "General/buffer.ML"
wenzelm@48514
    71
    "General/file.ML"
wenzelm@48514
    72
    "General/graph.ML"
wenzelm@49561
    73
    "General/graph_display.ML"
wenzelm@48514
    74
    "General/heap.ML"
wenzelm@48514
    75
    "General/integer.ML"
wenzelm@48514
    76
    "General/linear_set.ML"
wenzelm@48514
    77
    "General/long_name.ML"
wenzelm@48514
    78
    "General/name_space.ML"
wenzelm@48514
    79
    "General/ord_list.ML"
wenzelm@48514
    80
    "General/output.ML"
wenzelm@48514
    81
    "General/path.ML"
wenzelm@48514
    82
    "General/position.ML"
wenzelm@48514
    83
    "General/pretty.ML"
wenzelm@48514
    84
    "General/print_mode.ML"
wenzelm@48514
    85
    "General/properties.ML"
wenzelm@48514
    86
    "General/queue.ML"
wenzelm@48514
    87
    "General/same.ML"
wenzelm@48514
    88
    "General/scan.ML"
wenzelm@48514
    89
    "General/secure.ML"
wenzelm@48514
    90
    "General/seq.ML"
wenzelm@48514
    91
    "General/sha1.ML"
wenzelm@48514
    92
    "General/sha1_polyml.ML"
wenzelm@50800
    93
    "General/socket_io.ML"
wenzelm@48514
    94
    "General/source.ML"
wenzelm@48514
    95
    "General/stack.ML"
wenzelm@48514
    96
    "General/symbol.ML"
wenzelm@48514
    97
    "General/symbol_pos.ML"
wenzelm@48514
    98
    "General/table.ML"
wenzelm@48514
    99
    "General/timing.ML"
wenzelm@48514
   100
    "General/url.ML"
wenzelm@48514
   101
    "Isar/args.ML"
wenzelm@48514
   102
    "Isar/attrib.ML"
wenzelm@48514
   103
    "Isar/auto_bind.ML"
wenzelm@48514
   104
    "Isar/bundle.ML"
wenzelm@48514
   105
    "Isar/calculation.ML"
wenzelm@48514
   106
    "Isar/class.ML"
wenzelm@48514
   107
    "Isar/class_declaration.ML"
wenzelm@48514
   108
    "Isar/code.ML"
wenzelm@48514
   109
    "Isar/context_rules.ML"
wenzelm@48514
   110
    "Isar/element.ML"
wenzelm@48514
   111
    "Isar/expression.ML"
wenzelm@48514
   112
    "Isar/generic_target.ML"
wenzelm@48514
   113
    "Isar/isar_cmd.ML"
wenzelm@48514
   114
    "Isar/keyword.ML"
wenzelm@48514
   115
    "Isar/local_defs.ML"
wenzelm@48514
   116
    "Isar/local_theory.ML"
wenzelm@48514
   117
    "Isar/locale.ML"
wenzelm@48514
   118
    "Isar/method.ML"
wenzelm@48514
   119
    "Isar/named_target.ML"
wenzelm@48514
   120
    "Isar/object_logic.ML"
wenzelm@48514
   121
    "Isar/obtain.ML"
wenzelm@48514
   122
    "Isar/outer_syntax.ML"
wenzelm@48514
   123
    "Isar/overloading.ML"
wenzelm@48514
   124
    "Isar/parse.ML"
wenzelm@48514
   125
    "Isar/parse_spec.ML"
wenzelm@48514
   126
    "Isar/proof.ML"
wenzelm@48514
   127
    "Isar/proof_context.ML"
wenzelm@48514
   128
    "Isar/proof_display.ML"
wenzelm@48514
   129
    "Isar/proof_node.ML"
wenzelm@48514
   130
    "Isar/rule_cases.ML"
wenzelm@48514
   131
    "Isar/rule_insts.ML"
wenzelm@48514
   132
    "Isar/runtime.ML"
wenzelm@48514
   133
    "Isar/spec_rules.ML"
wenzelm@48514
   134
    "Isar/specification.ML"
wenzelm@48514
   135
    "Isar/token.ML"
wenzelm@48514
   136
    "Isar/toplevel.ML"
wenzelm@48514
   137
    "Isar/typedecl.ML"
wenzelm@52010
   138
    "ML/exn_properties_dummy.ML"
wenzelm@52010
   139
    "ML/exn_properties_polyml.ML"
wenzelm@48514
   140
    "ML/install_pp_polyml.ML"
wenzelm@48514
   141
    "ML/ml_antiquote.ML"
wenzelm@48514
   142
    "ML/ml_compiler.ML"
wenzelm@48514
   143
    "ML/ml_compiler_polyml.ML"
wenzelm@48514
   144
    "ML/ml_context.ML"
wenzelm@48514
   145
    "ML/ml_env.ML"
wenzelm@48514
   146
    "ML/ml_lex.ML"
wenzelm@48514
   147
    "ML/ml_parse.ML"
wenzelm@50255
   148
    "ML/ml_statistics_dummy.ML"
wenzelm@50255
   149
    "ML/ml_statistics_polyml-5.5.0.ML"
wenzelm@48514
   150
    "ML/ml_syntax.ML"
wenzelm@48514
   151
    "ML/ml_thms.ML"
wenzelm@50450
   152
    "PIDE/active.ML"
wenzelm@48514
   153
    "PIDE/command.ML"
wenzelm@48514
   154
    "PIDE/document.ML"
wenzelm@52530
   155
    "PIDE/document_id.ML"
wenzelm@52605
   156
    "PIDE/execution.ML"
wenzelm@48514
   157
    "PIDE/markup.ML"
wenzelm@48514
   158
    "PIDE/protocol.ML"
wenzelm@48514
   159
    "PIDE/xml.ML"
wenzelm@48514
   160
    "PIDE/yxml.ML"
wenzelm@48514
   161
    "Proof/extraction.ML"
wenzelm@48514
   162
    "Proof/proof_checker.ML"
wenzelm@48514
   163
    "Proof/proof_rewrite_rules.ML"
wenzelm@48514
   164
    "Proof/proof_syntax.ML"
wenzelm@48514
   165
    "Proof/reconstruct.ML"
wenzelm@48514
   166
    "ROOT.ML"
wenzelm@48514
   167
    "Syntax/ast.ML"
wenzelm@48514
   168
    "Syntax/lexicon.ML"
wenzelm@48514
   169
    "Syntax/local_syntax.ML"
wenzelm@48514
   170
    "Syntax/mixfix.ML"
wenzelm@48514
   171
    "Syntax/parser.ML"
wenzelm@48514
   172
    "Syntax/printer.ML"
wenzelm@48514
   173
    "Syntax/simple_syntax.ML"
wenzelm@48514
   174
    "Syntax/syntax.ML"
wenzelm@48514
   175
    "Syntax/syntax_ext.ML"
wenzelm@48514
   176
    "Syntax/syntax_phases.ML"
wenzelm@48514
   177
    "Syntax/syntax_trans.ML"
wenzelm@48514
   178
    "Syntax/term_position.ML"
wenzelm@52211
   179
    "Syntax/type_annotation.ML"
wenzelm@48681
   180
    "System/command_line.ML"
wenzelm@48514
   181
    "System/invoke_scala.ML"
wenzelm@48514
   182
    "System/isabelle_process.ML"
wenzelm@48514
   183
    "System/isabelle_system.ML"
wenzelm@48514
   184
    "System/isar.ML"
wenzelm@52584
   185
    "System/message_channel.ML"
wenzelm@48514
   186
    "System/options.ML"
wenzelm@48514
   187
    "System/session.ML"
wenzelm@48514
   188
    "System/system_channel.ML"
wenzelm@48514
   189
    "Thy/html.ML"
wenzelm@48514
   190
    "Thy/latex.ML"
wenzelm@48514
   191
    "Thy/present.ML"
wenzelm@48514
   192
    "Thy/rail.ML"
wenzelm@48514
   193
    "Thy/term_style.ML"
wenzelm@48514
   194
    "Thy/thm_deps.ML"
wenzelm@48514
   195
    "Thy/thy_header.ML"
wenzelm@48514
   196
    "Thy/thy_info.ML"
wenzelm@48514
   197
    "Thy/thy_load.ML"
wenzelm@48514
   198
    "Thy/thy_output.ML"
wenzelm@48514
   199
    "Thy/thy_syntax.ML"
wenzelm@50686
   200
    "Tools/build.ML"
wenzelm@52010
   201
    "Tools/legacy_xml_syntax.ML"
wenzelm@48514
   202
    "Tools/named_thms.ML"
wenzelm@52009
   203
    "Tools/proof_general.ML"
wenzelm@48514
   204
    "assumption.ML"
wenzelm@48514
   205
    "axclass.ML"
wenzelm@48514
   206
    "config.ML"
wenzelm@48514
   207
    "conjunction.ML"
wenzelm@48514
   208
    "consts.ML"
wenzelm@48514
   209
    "context.ML"
wenzelm@48514
   210
    "context_position.ML"
wenzelm@48514
   211
    "conv.ML"
wenzelm@48514
   212
    "defs.ML"
wenzelm@48514
   213
    "display.ML"
wenzelm@48514
   214
    "drule.ML"
wenzelm@48514
   215
    "envir.ML"
wenzelm@48514
   216
    "facts.ML"
wenzelm@48514
   217
    "global_theory.ML"
wenzelm@48514
   218
    "goal.ML"
wenzelm@48514
   219
    "goal_display.ML"
wenzelm@48514
   220
    "interpretation.ML"
wenzelm@48514
   221
    "item_net.ML"
wenzelm@48514
   222
    "library.ML"
wenzelm@48514
   223
    "logic.ML"
wenzelm@48514
   224
    "more_thm.ML"
wenzelm@48514
   225
    "morphism.ML"
wenzelm@48514
   226
    "name.ML"
wenzelm@48514
   227
    "net.ML"
wenzelm@48514
   228
    "pattern.ML"
wenzelm@48514
   229
    "primitive_defs.ML"
wenzelm@48514
   230
    "proofterm.ML"
wenzelm@48879
   231
    "pure_syn.ML"
wenzelm@48514
   232
    "pure_thy.ML"
wenzelm@48514
   233
    "raw_simplifier.ML"
wenzelm@48514
   234
    "search.ML"
wenzelm@48514
   235
    "sign.ML"
wenzelm@48514
   236
    "simplifier.ML"
wenzelm@51551
   237
    "skip_proof.ML"
wenzelm@48514
   238
    "sorts.ML"
wenzelm@48514
   239
    "subgoal.ML"
wenzelm@48514
   240
    "tactic.ML"
wenzelm@48514
   241
    "tactical.ML"
wenzelm@48514
   242
    "term.ML"
wenzelm@48514
   243
    "term_ord.ML"
wenzelm@48514
   244
    "term_sharing.ML"
wenzelm@48514
   245
    "term_subst.ML"
wenzelm@48514
   246
    "term_xml.ML"
wenzelm@48514
   247
    "theory.ML"
wenzelm@48514
   248
    "thm.ML"
wenzelm@48514
   249
    "type.ML"
wenzelm@48514
   250
    "type_infer.ML"
wenzelm@48514
   251
    "type_infer_context.ML"
wenzelm@48514
   252
    "unify.ML"
wenzelm@48514
   253
    "variable.ML"
wenzelm@48514
   254