1.1 --- a/src/Pure/ROOT Thu Jul 26 13:38:43 2012 +0200
1.2 +++ b/src/Pure/ROOT Thu Jul 26 14:22:37 2012 +0200
1.3 @@ -21,5 +21,233 @@
1.4
1.5 session Pure in "." =
1.6 theories Pure
1.7 - files "ROOT.ML" (* FIXME *)
1.8 + files
1.9 + "General/exn.ML"
1.10 + "ML-Systems/compiler_polyml.ML"
1.11 + "ML-Systems/ml_name_space.ML"
1.12 + "ML-Systems/ml_pretty.ML"
1.13 + "ML-Systems/ml_system.ML"
1.14 + "ML-Systems/multithreading.ML"
1.15 + "ML-Systems/multithreading_polyml.ML"
1.16 + "ML-Systems/overloading_smlnj.ML"
1.17 + "ML-Systems/polyml.ML"
1.18 + "ML-Systems/pp_dummy.ML"
1.19 + "ML-Systems/proper_int.ML"
1.20 + "ML-Systems/single_assignment.ML"
1.21 + "ML-Systems/single_assignment_polyml.ML"
1.22 + "ML-Systems/smlnj.ML"
1.23 + "ML-Systems/thread_dummy.ML"
1.24 + "ML-Systems/universal.ML"
1.25 + "ML-Systems/unsynchronized.ML"
1.26 + "ML-Systems/use_context.ML"
1.27
1.28 + "Concurrent/bash.ML"
1.29 + "Concurrent/bash_sequential.ML"
1.30 + "Concurrent/cache.ML"
1.31 + "Concurrent/future.ML"
1.32 + "Concurrent/lazy.ML"
1.33 + "Concurrent/lazy_sequential.ML"
1.34 + "Concurrent/mailbox.ML"
1.35 + "Concurrent/par_exn.ML"
1.36 + "Concurrent/par_list.ML"
1.37 + "Concurrent/par_list_sequential.ML"
1.38 + "Concurrent/simple_thread.ML"
1.39 + "Concurrent/single_assignment.ML"
1.40 + "Concurrent/single_assignment_sequential.ML"
1.41 + "Concurrent/synchronized.ML"
1.42 + "Concurrent/synchronized_sequential.ML"
1.43 + "Concurrent/task_queue.ML"
1.44 + "Concurrent/time_limit.ML"
1.45 + "General/alist.ML"
1.46 + "General/antiquote.ML"
1.47 + "General/balanced_tree.ML"
1.48 + "General/basics.ML"
1.49 + "General/binding.ML"
1.50 + "General/buffer.ML"
1.51 + "General/file.ML"
1.52 + "General/graph.ML"
1.53 + "General/heap.ML"
1.54 + "General/integer.ML"
1.55 + "General/linear_set.ML"
1.56 + "General/long_name.ML"
1.57 + "General/name_space.ML"
1.58 + "General/ord_list.ML"
1.59 + "General/output.ML"
1.60 + "General/path.ML"
1.61 + "General/position.ML"
1.62 + "General/pretty.ML"
1.63 + "General/print_mode.ML"
1.64 + "General/properties.ML"
1.65 + "General/queue.ML"
1.66 + "General/same.ML"
1.67 + "General/scan.ML"
1.68 + "General/secure.ML"
1.69 + "General/seq.ML"
1.70 + "General/sha1.ML"
1.71 + "General/sha1_polyml.ML"
1.72 + "General/source.ML"
1.73 + "General/stack.ML"
1.74 + "General/symbol.ML"
1.75 + "General/symbol_pos.ML"
1.76 + "General/table.ML"
1.77 + "General/timing.ML"
1.78 + "General/url.ML"
1.79 + "Isar/args.ML"
1.80 + "Isar/attrib.ML"
1.81 + "Isar/auto_bind.ML"
1.82 + "Isar/bundle.ML"
1.83 + "Isar/calculation.ML"
1.84 + "Isar/class.ML"
1.85 + "Isar/class_declaration.ML"
1.86 + "Isar/code.ML"
1.87 + "Isar/context_rules.ML"
1.88 + "Isar/element.ML"
1.89 + "Isar/expression.ML"
1.90 + "Isar/generic_target.ML"
1.91 + "Isar/isar_cmd.ML"
1.92 + "Isar/isar_syn.ML"
1.93 + "Isar/keyword.ML"
1.94 + "Isar/local_defs.ML"
1.95 + "Isar/local_theory.ML"
1.96 + "Isar/locale.ML"
1.97 + "Isar/method.ML"
1.98 + "Isar/named_target.ML"
1.99 + "Isar/object_logic.ML"
1.100 + "Isar/obtain.ML"
1.101 + "Isar/outer_syntax.ML"
1.102 + "Isar/overloading.ML"
1.103 + "Isar/parse.ML"
1.104 + "Isar/parse_spec.ML"
1.105 + "Isar/proof.ML"
1.106 + "Isar/proof_context.ML"
1.107 + "Isar/proof_display.ML"
1.108 + "Isar/proof_node.ML"
1.109 + "Isar/rule_cases.ML"
1.110 + "Isar/rule_insts.ML"
1.111 + "Isar/runtime.ML"
1.112 + "Isar/skip_proof.ML"
1.113 + "Isar/spec_rules.ML"
1.114 + "Isar/specification.ML"
1.115 + "Isar/token.ML"
1.116 + "Isar/toplevel.ML"
1.117 + "Isar/typedecl.ML"
1.118 + "ML/install_pp_polyml.ML"
1.119 + "ML/ml_antiquote.ML"
1.120 + "ML/ml_compiler.ML"
1.121 + "ML/ml_compiler_polyml.ML"
1.122 + "ML/ml_context.ML"
1.123 + "ML/ml_env.ML"
1.124 + "ML/ml_lex.ML"
1.125 + "ML/ml_parse.ML"
1.126 + "ML/ml_syntax.ML"
1.127 + "ML/ml_thms.ML"
1.128 + "PIDE/command.ML"
1.129 + "PIDE/document.ML"
1.130 + "PIDE/isabelle_markup.ML"
1.131 + "PIDE/markup.ML"
1.132 + "PIDE/protocol.ML"
1.133 + "PIDE/xml.ML"
1.134 + "PIDE/yxml.ML"
1.135 + "Proof/extraction.ML"
1.136 + "Proof/proof_checker.ML"
1.137 + "Proof/proof_rewrite_rules.ML"
1.138 + "Proof/proof_syntax.ML"
1.139 + "Proof/reconstruct.ML"
1.140 + "ProofGeneral/pgip.ML"
1.141 + "ProofGeneral/pgip_input.ML"
1.142 + "ProofGeneral/pgip_isabelle.ML"
1.143 + "ProofGeneral/pgip_markup.ML"
1.144 + "ProofGeneral/pgip_output.ML"
1.145 + "ProofGeneral/pgip_parser.ML"
1.146 + "ProofGeneral/pgip_tests.ML"
1.147 + "ProofGeneral/pgip_types.ML"
1.148 + "ProofGeneral/pgml.ML"
1.149 + "ProofGeneral/preferences.ML"
1.150 + "ProofGeneral/proof_general_emacs.ML"
1.151 + "ProofGeneral/proof_general_pgip.ML"
1.152 + "ROOT.ML"
1.153 + "Syntax/ast.ML"
1.154 + "Syntax/lexicon.ML"
1.155 + "Syntax/local_syntax.ML"
1.156 + "Syntax/mixfix.ML"
1.157 + "Syntax/parser.ML"
1.158 + "Syntax/printer.ML"
1.159 + "Syntax/simple_syntax.ML"
1.160 + "Syntax/syntax.ML"
1.161 + "Syntax/syntax_ext.ML"
1.162 + "Syntax/syntax_phases.ML"
1.163 + "Syntax/syntax_trans.ML"
1.164 + "Syntax/term_position.ML"
1.165 + "System/build.ML"
1.166 + "System/invoke_scala.ML"
1.167 + "System/isabelle_process.ML"
1.168 + "System/isabelle_system.ML"
1.169 + "System/isar.ML"
1.170 + "System/options.ML"
1.171 + "System/session.ML"
1.172 + "System/system_channel.ML"
1.173 + "Thy/html.ML"
1.174 + "Thy/latex.ML"
1.175 + "Thy/present.ML"
1.176 + "Thy/rail.ML"
1.177 + "Thy/term_style.ML"
1.178 + "Thy/thm_deps.ML"
1.179 + "Thy/thy_header.ML"
1.180 + "Thy/thy_info.ML"
1.181 + "Thy/thy_load.ML"
1.182 + "Thy/thy_output.ML"
1.183 + "Thy/thy_syntax.ML"
1.184 + "Tools/find_consts.ML"
1.185 + "Tools/find_theorems.ML"
1.186 + "Tools/named_thms.ML"
1.187 + "Tools/xml_syntax.ML"
1.188 + "assumption.ML"
1.189 + "axclass.ML"
1.190 + "config.ML"
1.191 + "conjunction.ML"
1.192 + "consts.ML"
1.193 + "context.ML"
1.194 + "context_position.ML"
1.195 + "conv.ML"
1.196 + "defs.ML"
1.197 + "display.ML"
1.198 + "drule.ML"
1.199 + "envir.ML"
1.200 + "facts.ML"
1.201 + "global_theory.ML"
1.202 + "goal.ML"
1.203 + "goal_display.ML"
1.204 + "interpretation.ML"
1.205 + "item_net.ML"
1.206 + "library.ML"
1.207 + "logic.ML"
1.208 + "more_thm.ML"
1.209 + "morphism.ML"
1.210 + "name.ML"
1.211 + "net.ML"
1.212 + "pattern.ML"
1.213 + "primitive_defs.ML"
1.214 + "proofterm.ML"
1.215 + "pure_setup.ML"
1.216 + "pure_thy.ML"
1.217 + "raw_simplifier.ML"
1.218 + "search.ML"
1.219 + "sign.ML"
1.220 + "simplifier.ML"
1.221 + "sorts.ML"
1.222 + "subgoal.ML"
1.223 + "tactic.ML"
1.224 + "tactical.ML"
1.225 + "term.ML"
1.226 + "term_ord.ML"
1.227 + "term_sharing.ML"
1.228 + "term_subst.ML"
1.229 + "term_xml.ML"
1.230 + "theory.ML"
1.231 + "thm.ML"
1.232 + "type.ML"
1.233 + "type_infer.ML"
1.234 + "type_infer_context.ML"
1.235 + "unify.ML"
1.236 + "variable.ML"
1.237 +