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