2006-02-16 obua [Thu, 16 Feb 2006 03:23:57 +0100] rev 19066
adapted to kernel changes
src/HOL/Import/proof_kernel.ML

2006-02-16 wenzelm [Thu, 16 Feb 2006 00:09:46 +0100] rev 19065
tuned subst_bound(s);
src/Pure/term.ML

2006-02-15 obua [Wed, 15 Feb 2006 23:57:06 +0100] rev 19064
fixed bugs, added caching
src/HOL/Import/Generate-HOLLight/GenHOLLight.thy src/HOL/Import/HOL4Compat.thy src/HOL/Import/HOL4Setup.thy src/HOL/Import/HOLLightCompat.thy src/HOL/Import/ImportRecorder.thy src/HOL/Import/import_syntax.ML src/HOL/Import/importrecorder.ML src/HOL/Import/lazy_scan.ML src/HOL/Import/lazy_seq.ML src/HOL/Import/proof_kernel.ML src/HOL/Import/replay.ML src/HOL/Import/xml.ML src/HOL/Import/xmlconv.ML

2006-02-15 wenzelm [Wed, 15 Feb 2006 21:35:13 +0100] rev 19063
added cases_node;
replaced body_context_of by body_context_node, removed no_body_context;
copy: ProofContext.transfer;
added present_local_theory, present_proof;
removed internal command interface;
src/Pure/Isar/toplevel.ML

2006-02-15 wenzelm [Wed, 15 Feb 2006 21:35:12 +0100] rev 19062
replaced qualified_force_prefix to sticky_prefix;
do not export read_terms;
src/Pure/Isar/proof_context.ML

2006-02-15 wenzelm [Wed, 15 Feb 2006 21:35:11 +0100] rev 19061
removed distinct, renamed gen_distinct to distinct;
replaced qualified_force_prefix by qualified_names/sticky_prefix;
src/Pure/Isar/locale.ML

2006-02-15 wenzelm [Wed, 15 Feb 2006 21:35:11 +0100] rev 19060
check_text: Toplevel.node option;
src/Pure/Isar/outer_syntax.ML

2006-02-15 wenzelm [Wed, 15 Feb 2006 21:35:09 +0100] rev 19059
init/exit no longer change the theory (no naming);
added naming, restore_naming, mapping;
src/Pure/Isar/local_theory.ML

2006-02-15 wenzelm [Wed, 15 Feb 2006 21:35:09 +0100] rev 19058
evaluate antiquotes depending on Toplevel.node option;
src/Pure/Isar/isar_output.ML

2006-02-15 wenzelm [Wed, 15 Feb 2006 21:35:07 +0100] rev 19057
simplified presentation commands;
src/Pure/Isar/isar_cmd.ML