src/Pure/ROOT
author blanchet
Fri, 20 Dec 2013 20:36:38 +0100
changeset 54838 16511f84913c
parent 54723 124432e77ecf
child 55030 9a9049d12e21
permissions -rw-r--r--
reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
51397
03b586ee5930 support for 'chapter' specifications within session ROOT;
wenzelm
parents: 50911
diff changeset
     1
chapter Pure
03b586ee5930 support for 'chapter' specifications within session ROOT;
wenzelm
parents: 50911
diff changeset
     2
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48732
diff changeset
     3
session RAW =
48916
f45ccc0d1ace clarified syntax boundary cases and errors;
wenzelm
parents: 48879
diff changeset
     4
  theories
48347
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
     5
  files
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
     6
    "General/exn.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
     7
    "ML-Systems/compiler_polyml.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
     8
    "ML-Systems/ml_name_space.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
     9
    "ML-Systems/ml_pretty.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
    10
    "ML-Systems/ml_system.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
    11
    "ML-Systems/multithreading.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
    12
    "ML-Systems/multithreading_polyml.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
    13
    "ML-Systems/overloading_smlnj.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
    14
    "ML-Systems/polyml.ML"
54723
124432e77ecf simplified polyml-5.5.2 setup -- implicit upgrade of Thread.numProcessors;
wenzelm
parents: 54717
diff changeset
    15
    "ML-Systems/polyml-5.5.2.ML"
48347
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
    16
    "ML-Systems/pp_dummy.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
    17
    "ML-Systems/proper_int.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
    18
    "ML-Systems/single_assignment.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
    19
    "ML-Systems/single_assignment_polyml.ML"
52711
155f02cacb2d old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);
wenzelm
parents: 52605
diff changeset
    20
    "ML-Systems/share_common_data_polyml-5.3.0.ML"
48347
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
    21
    "ML-Systems/smlnj.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
    22
    "ML-Systems/thread_dummy.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
    23
    "ML-Systems/universal.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
    24
    "ML-Systems/unsynchronized.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
    25
    "ML-Systems/use_context.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
    26
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48732
diff changeset
    27
session Pure =
48422
9613780a805b determine source dependencies, relatively to preloaded theories;
wenzelm
parents: 48347
diff changeset
    28
  theories Pure
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    29
  files
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    30
    "General/exn.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    31
    "ML-Systems/compiler_polyml.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    32
    "ML-Systems/ml_name_space.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    33
    "ML-Systems/ml_pretty.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    34
    "ML-Systems/ml_system.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    35
    "ML-Systems/multithreading.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    36
    "ML-Systems/multithreading_polyml.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    37
    "ML-Systems/overloading_smlnj.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    38
    "ML-Systems/polyml.ML"
54723
124432e77ecf simplified polyml-5.5.2 setup -- implicit upgrade of Thread.numProcessors;
wenzelm
parents: 54717
diff changeset
    39
    "ML-Systems/polyml-5.5.2.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    40
    "ML-Systems/pp_dummy.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    41
    "ML-Systems/proper_int.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    42
    "ML-Systems/single_assignment.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    43
    "ML-Systems/single_assignment_polyml.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    44
    "ML-Systems/smlnj.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    45
    "ML-Systems/thread_dummy.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    46
    "ML-Systems/universal.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    47
    "ML-Systems/unsynchronized.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    48
    "ML-Systems/use_context.ML"
48347
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
    49
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    50
    "Concurrent/bash.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    51
    "Concurrent/bash_sequential.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    52
    "Concurrent/cache.ML"
52050
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents: 52010
diff changeset
    53
    "Concurrent/event_timer.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    54
    "Concurrent/future.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    55
    "Concurrent/lazy.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    56
    "Concurrent/lazy_sequential.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    57
    "Concurrent/mailbox.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    58
    "Concurrent/par_exn.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    59
    "Concurrent/par_list.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    60
    "Concurrent/par_list_sequential.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    61
    "Concurrent/simple_thread.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    62
    "Concurrent/single_assignment.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    63
    "Concurrent/single_assignment_sequential.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    64
    "Concurrent/synchronized.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    65
    "Concurrent/synchronized_sequential.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    66
    "Concurrent/task_queue.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    67
    "Concurrent/time_limit.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    68
    "General/alist.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    69
    "General/antiquote.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    70
    "General/balanced_tree.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    71
    "General/basics.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    72
    "General/binding.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    73
    "General/buffer.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    74
    "General/file.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    75
    "General/graph.ML"
49561
26fc70e983c2 separate module Graph_Display;
wenzelm
parents: 48916
diff changeset
    76
    "General/graph_display.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    77
    "General/heap.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    78
    "General/integer.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    79
    "General/linear_set.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    80
    "General/long_name.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    81
    "General/name_space.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    82
    "General/ord_list.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    83
    "General/output.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    84
    "General/path.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    85
    "General/position.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    86
    "General/pretty.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    87
    "General/print_mode.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    88
    "General/properties.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    89
    "General/queue.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    90
    "General/same.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    91
    "General/scan.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    92
    "General/secure.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    93
    "General/seq.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    94
    "General/sha1.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    95
    "General/sha1_polyml.ML"
53212
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents: 52926
diff changeset
    96
    "General/sha1_samples.ML"
50800
c0fb2839d1a9 recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents: 50686
diff changeset
    97
    "General/socket_io.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    98
    "General/source.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    99
    "General/stack.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   100
    "General/symbol.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   101
    "General/symbol_pos.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   102
    "General/table.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   103
    "General/timing.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   104
    "General/url.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   105
    "Isar/args.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   106
    "Isar/attrib.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   107
    "Isar/auto_bind.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   108
    "Isar/bundle.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   109
    "Isar/calculation.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   110
    "Isar/class.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   111
    "Isar/class_declaration.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   112
    "Isar/code.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   113
    "Isar/context_rules.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   114
    "Isar/element.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   115
    "Isar/expression.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   116
    "Isar/generic_target.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   117
    "Isar/isar_cmd.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   118
    "Isar/keyword.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   119
    "Isar/local_defs.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   120
    "Isar/local_theory.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   121
    "Isar/locale.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   122
    "Isar/method.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   123
    "Isar/named_target.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   124
    "Isar/object_logic.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   125
    "Isar/obtain.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   126
    "Isar/outer_syntax.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   127
    "Isar/overloading.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   128
    "Isar/parse.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   129
    "Isar/parse_spec.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   130
    "Isar/proof.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   131
    "Isar/proof_context.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   132
    "Isar/proof_display.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   133
    "Isar/proof_node.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   134
    "Isar/rule_cases.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   135
    "Isar/runtime.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   136
    "Isar/spec_rules.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   137
    "Isar/specification.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   138
    "Isar/token.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   139
    "Isar/toplevel.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   140
    "Isar/typedecl.ML"
52010
wenzelm
parents: 52009
diff changeset
   141
    "ML/exn_properties_dummy.ML"
wenzelm
parents: 52009
diff changeset
   142
    "ML/exn_properties_polyml.ML"
52836
1a03ffc00a4a exception trace for Poly/ML 5.5.1, using regular Isabelle output;
wenzelm
parents: 52711
diff changeset
   143
    "ML/exn_trace_polyml-5.5.1.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   144
    "ML/install_pp_polyml.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   145
    "ML/ml_antiquote.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   146
    "ML/ml_compiler.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   147
    "ML/ml_compiler_polyml.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   148
    "ML/ml_context.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   149
    "ML/ml_env.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   150
    "ML/ml_lex.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   151
    "ML/ml_parse.ML"
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50217
diff changeset
   152
    "ML/ml_statistics_dummy.ML"
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50217
diff changeset
   153
    "ML/ml_statistics_polyml-5.5.0.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   154
    "ML/ml_syntax.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   155
    "ML/ml_thms.ML"
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50255
diff changeset
   156
    "PIDE/active.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   157
    "PIDE/command.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   158
    "PIDE/document.ML"
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52211
diff changeset
   159
    "PIDE/document_id.ML"
52605
a2a805549c74 clarified module name;
wenzelm
parents: 52596
diff changeset
   160
    "PIDE/execution.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   161
    "PIDE/markup.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   162
    "PIDE/protocol.ML"
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents: 52836
diff changeset
   163
    "PIDE/query_operation.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   164
    "PIDE/xml.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   165
    "PIDE/yxml.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   166
    "Proof/extraction.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   167
    "Proof/proof_checker.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   168
    "Proof/proof_rewrite_rules.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   169
    "Proof/proof_syntax.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   170
    "Proof/reconstruct.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   171
    "ROOT.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   172
    "Syntax/ast.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   173
    "Syntax/lexicon.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   174
    "Syntax/local_syntax.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   175
    "Syntax/mixfix.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   176
    "Syntax/parser.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   177
    "Syntax/printer.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   178
    "Syntax/simple_syntax.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   179
    "Syntax/syntax.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   180
    "Syntax/syntax_ext.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   181
    "Syntax/syntax_phases.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   182
    "Syntax/syntax_trans.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   183
    "Syntax/term_position.ML"
52211
66bc827e37f8 explicit support for type annotations within printed syntax trees;
wenzelm
parents: 52050
diff changeset
   184
    "Syntax/type_annotation.ML"
48681
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version);
wenzelm
parents: 48646
diff changeset
   185
    "System/command_line.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   186
    "System/invoke_scala.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   187
    "System/isabelle_process.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   188
    "System/isabelle_system.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   189
    "System/isar.ML"
52584
5cad4a5f5615 more abstract message channel;
wenzelm
parents: 52530
diff changeset
   190
    "System/message_channel.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   191
    "System/options.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   192
    "System/session.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   193
    "System/system_channel.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   194
    "Thy/html.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   195
    "Thy/latex.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   196
    "Thy/present.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   197
    "Thy/rail.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   198
    "Thy/term_style.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   199
    "Thy/thm_deps.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   200
    "Thy/thy_header.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   201
    "Thy/thy_info.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   202
    "Thy/thy_load.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   203
    "Thy/thy_output.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   204
    "Thy/thy_syntax.ML"
50686
d703e3aafa8c moved files;
wenzelm
parents: 50450
diff changeset
   205
    "Tools/build.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   206
    "Tools/named_thms.ML"
52009
3b18ef9df768 moved files;
wenzelm
parents: 52007
diff changeset
   207
    "Tools/proof_general.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   208
    "assumption.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   209
    "axclass.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   210
    "config.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   211
    "conjunction.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   212
    "consts.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   213
    "context.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   214
    "context_position.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   215
    "conv.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   216
    "defs.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   217
    "display.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   218
    "drule.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   219
    "envir.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   220
    "facts.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   221
    "global_theory.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   222
    "goal.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   223
    "goal_display.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   224
    "interpretation.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   225
    "item_net.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   226
    "library.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   227
    "logic.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   228
    "more_thm.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   229
    "morphism.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   230
    "name.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   231
    "net.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   232
    "pattern.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   233
    "primitive_defs.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   234
    "proofterm.ML"
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents: 48738
diff changeset
   235
    "pure_syn.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   236
    "pure_thy.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   237
    "raw_simplifier.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   238
    "search.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   239
    "sign.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   240
    "simplifier.ML"
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51397
diff changeset
   241
    "skip_proof.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   242
    "sorts.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   243
    "subgoal.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   244
    "tactic.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   245
    "tactical.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   246
    "term.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   247
    "term_ord.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   248
    "term_sharing.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   249
    "term_subst.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   250
    "term_xml.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   251
    "theory.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   252
    "thm.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   253
    "type.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   254
    "type_infer.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   255
    "type_infer_context.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   256
    "unify.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   257
    "variable.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   258