2008-04-13 wenzelm removed unused minimal_classes;
2008-04-13 wenzelm added insert_sorts (from thm.ML);
2008-04-13 wenzelm tsig: removed unnecessary universal witness;
2008-04-13 wenzelm tuned;
2008-04-12 wenzelm removed unnecessary Goal.close_result;
2008-04-12 wenzelm replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2008-04-12 wenzelm advance: do not count utf8 trailer bytes (which happen to be undefined or punctuation in iso-latin);
2008-04-12 wenzelm added is_utf8_trailer;
2008-04-12 wenzelm rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-12 wenzelm obsolete -- Poly/ML images are maximally shared already, home-grown compression wastes space and time;
2008-04-12 wenzelm removed obsolete compress.ML
2008-04-12 wenzelm replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2008-04-12 wenzelm rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-12 wenzelm rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-10 wenzelm use_text: explicitly print exception, which is no longer done by the new PolyML.compiler setup;
2008-04-10 wenzelm transaction/init: ensure stable theory (non-draft);
2008-04-10 wenzelm export is_draft, not draftN;
2008-04-10 wenzelm simplified isarcmd;
2008-04-10 wenzelm eliminated unused name_of, source, source_of, print', print3, three_buffersN;
2008-04-10 wenzelm eliminated unused trace, read;
2008-04-10 wenzelm eliminated unused Toplevel.print3/three_buffers;
2008-04-10 wenzelm tuned;
2008-04-10 wenzelm Isar.goal: tactical goal only;
2008-04-10 wenzelm eliminated backpatching of load_thy;
2008-04-10 wenzelm added read_const_exprs (from Pure/Isar/code_unit.ML);
2008-04-10 wenzelm export get_names (formerly names);
2008-04-10 wenzelm ThyInfo.get_names;
2008-04-10 wenzelm ThyInfo.get_theory;
2008-04-10 wenzelm export load_thy -- no backpatching;
2008-04-10 wenzelm export subst_alias;
2008-04-10 wenzelm load thy_info.ML after outer_syntax.ML -- avoids backpatching of load_thy;
2008-04-10 wenzelm val theory = ThyInfo.get_theory;
(0) -10000 -3000 -1000 -300 -100 -50 -32 +32 +50 +100 +300 +1000 +3000 +10000 +30000 tip