--- a/src/Pure/ROOT Thu Jul 26 13:38:43 2012 +0200
+++ b/src/Pure/ROOT Thu Jul 26 14:22:37 2012 +0200
@@ -21,5 +21,233 @@
session Pure in "." =
theories Pure
- files "ROOT.ML" (* FIXME *)
+ files
+ "General/exn.ML"
+ "ML-Systems/compiler_polyml.ML"
+ "ML-Systems/ml_name_space.ML"
+ "ML-Systems/ml_pretty.ML"
+ "ML-Systems/ml_system.ML"
+ "ML-Systems/multithreading.ML"
+ "ML-Systems/multithreading_polyml.ML"
+ "ML-Systems/overloading_smlnj.ML"
+ "ML-Systems/polyml.ML"
+ "ML-Systems/pp_dummy.ML"
+ "ML-Systems/proper_int.ML"
+ "ML-Systems/single_assignment.ML"
+ "ML-Systems/single_assignment_polyml.ML"
+ "ML-Systems/smlnj.ML"
+ "ML-Systems/thread_dummy.ML"
+ "ML-Systems/universal.ML"
+ "ML-Systems/unsynchronized.ML"
+ "ML-Systems/use_context.ML"
+ "Concurrent/bash.ML"
+ "Concurrent/bash_sequential.ML"
+ "Concurrent/cache.ML"
+ "Concurrent/future.ML"
+ "Concurrent/lazy.ML"
+ "Concurrent/lazy_sequential.ML"
+ "Concurrent/mailbox.ML"
+ "Concurrent/par_exn.ML"
+ "Concurrent/par_list.ML"
+ "Concurrent/par_list_sequential.ML"
+ "Concurrent/simple_thread.ML"
+ "Concurrent/single_assignment.ML"
+ "Concurrent/single_assignment_sequential.ML"
+ "Concurrent/synchronized.ML"
+ "Concurrent/synchronized_sequential.ML"
+ "Concurrent/task_queue.ML"
+ "Concurrent/time_limit.ML"
+ "General/alist.ML"
+ "General/antiquote.ML"
+ "General/balanced_tree.ML"
+ "General/basics.ML"
+ "General/binding.ML"
+ "General/buffer.ML"
+ "General/file.ML"
+ "General/graph.ML"
+ "General/heap.ML"
+ "General/integer.ML"
+ "General/linear_set.ML"
+ "General/long_name.ML"
+ "General/name_space.ML"
+ "General/ord_list.ML"
+ "General/output.ML"
+ "General/path.ML"
+ "General/position.ML"
+ "General/pretty.ML"
+ "General/print_mode.ML"
+ "General/properties.ML"
+ "General/queue.ML"
+ "General/same.ML"
+ "General/scan.ML"
+ "General/secure.ML"
+ "General/seq.ML"
+ "General/sha1.ML"
+ "General/sha1_polyml.ML"
+ "General/source.ML"
+ "General/stack.ML"
+ "General/symbol.ML"
+ "General/symbol_pos.ML"
+ "General/table.ML"
+ "General/timing.ML"
+ "General/url.ML"
+ "Isar/args.ML"
+ "Isar/attrib.ML"
+ "Isar/auto_bind.ML"
+ "Isar/bundle.ML"
+ "Isar/calculation.ML"
+ "Isar/class.ML"
+ "Isar/class_declaration.ML"
+ "Isar/code.ML"
+ "Isar/context_rules.ML"
+ "Isar/element.ML"
+ "Isar/expression.ML"
+ "Isar/generic_target.ML"
+ "Isar/isar_cmd.ML"
+ "Isar/isar_syn.ML"
+ "Isar/keyword.ML"
+ "Isar/local_defs.ML"
+ "Isar/local_theory.ML"
+ "Isar/locale.ML"
+ "Isar/method.ML"
+ "Isar/named_target.ML"
+ "Isar/object_logic.ML"
+ "Isar/obtain.ML"
+ "Isar/outer_syntax.ML"
+ "Isar/overloading.ML"
+ "Isar/parse.ML"
+ "Isar/parse_spec.ML"
+ "Isar/proof.ML"
+ "Isar/proof_context.ML"
+ "Isar/proof_display.ML"
+ "Isar/proof_node.ML"
+ "Isar/rule_cases.ML"
+ "Isar/rule_insts.ML"
+ "Isar/runtime.ML"
+ "Isar/skip_proof.ML"
+ "Isar/spec_rules.ML"
+ "Isar/specification.ML"
+ "Isar/token.ML"
+ "Isar/toplevel.ML"
+ "Isar/typedecl.ML"
+ "ML/install_pp_polyml.ML"
+ "ML/ml_antiquote.ML"
+ "ML/ml_compiler.ML"
+ "ML/ml_compiler_polyml.ML"
+ "ML/ml_context.ML"
+ "ML/ml_env.ML"
+ "ML/ml_lex.ML"
+ "ML/ml_parse.ML"
+ "ML/ml_syntax.ML"
+ "ML/ml_thms.ML"
+ "PIDE/command.ML"
+ "PIDE/document.ML"
+ "PIDE/isabelle_markup.ML"
+ "PIDE/markup.ML"
+ "PIDE/protocol.ML"
+ "PIDE/xml.ML"
+ "PIDE/yxml.ML"
+ "Proof/extraction.ML"
+ "Proof/proof_checker.ML"
+ "Proof/proof_rewrite_rules.ML"
+ "Proof/proof_syntax.ML"
+ "Proof/reconstruct.ML"
+ "ProofGeneral/pgip.ML"
+ "ProofGeneral/pgip_input.ML"
+ "ProofGeneral/pgip_isabelle.ML"
+ "ProofGeneral/pgip_markup.ML"
+ "ProofGeneral/pgip_output.ML"
+ "ProofGeneral/pgip_parser.ML"
+ "ProofGeneral/pgip_tests.ML"
+ "ProofGeneral/pgip_types.ML"
+ "ProofGeneral/pgml.ML"
+ "ProofGeneral/preferences.ML"
+ "ProofGeneral/proof_general_emacs.ML"
+ "ProofGeneral/proof_general_pgip.ML"
+ "ROOT.ML"
+ "Syntax/ast.ML"
+ "Syntax/lexicon.ML"
+ "Syntax/local_syntax.ML"
+ "Syntax/mixfix.ML"
+ "Syntax/parser.ML"
+ "Syntax/printer.ML"
+ "Syntax/simple_syntax.ML"
+ "Syntax/syntax.ML"
+ "Syntax/syntax_ext.ML"
+ "Syntax/syntax_phases.ML"
+ "Syntax/syntax_trans.ML"
+ "Syntax/term_position.ML"
+ "System/build.ML"
+ "System/invoke_scala.ML"
+ "System/isabelle_process.ML"
+ "System/isabelle_system.ML"
+ "System/isar.ML"
+ "System/options.ML"
+ "System/session.ML"
+ "System/system_channel.ML"
+ "Thy/html.ML"
+ "Thy/latex.ML"
+ "Thy/present.ML"
+ "Thy/rail.ML"
+ "Thy/term_style.ML"
+ "Thy/thm_deps.ML"
+ "Thy/thy_header.ML"
+ "Thy/thy_info.ML"
+ "Thy/thy_load.ML"
+ "Thy/thy_output.ML"
+ "Thy/thy_syntax.ML"
+ "Tools/find_consts.ML"
+ "Tools/find_theorems.ML"
+ "Tools/named_thms.ML"
+ "Tools/xml_syntax.ML"
+ "assumption.ML"
+ "axclass.ML"
+ "config.ML"
+ "conjunction.ML"
+ "consts.ML"
+ "context.ML"
+ "context_position.ML"
+ "conv.ML"
+ "defs.ML"
+ "display.ML"
+ "drule.ML"
+ "envir.ML"
+ "facts.ML"
+ "global_theory.ML"
+ "goal.ML"
+ "goal_display.ML"
+ "interpretation.ML"
+ "item_net.ML"
+ "library.ML"
+ "logic.ML"
+ "more_thm.ML"
+ "morphism.ML"
+ "name.ML"
+ "net.ML"
+ "pattern.ML"
+ "primitive_defs.ML"
+ "proofterm.ML"
+ "pure_setup.ML"
+ "pure_thy.ML"
+ "raw_simplifier.ML"
+ "search.ML"
+ "sign.ML"
+ "simplifier.ML"
+ "sorts.ML"
+ "subgoal.ML"
+ "tactic.ML"
+ "tactical.ML"
+ "term.ML"
+ "term_ord.ML"
+ "term_sharing.ML"
+ "term_subst.ML"
+ "term_xml.ML"
+ "theory.ML"
+ "thm.ML"
+ "type.ML"
+ "type_infer.ML"
+ "type_infer_context.ML"
+ "unify.ML"
+ "variable.ML"
+