# HG changeset patch # User wenzelm # Date 1343305357 -7200 # Node ID 84df8858c8acc0edd5668355103f28b438b3a500 # Parent ace120a2cb70320de4ae83632e38b02c5bb1b227 more files for session Pure; diff -r ace120a2cb70 -r 84df8858c8ac src/Pure/ROOT --- 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" +