2008-04-14 krauss proper context for induct_scheme method
2008-04-14 wenzelm Isar.toplevel_loop: separate init/welcome flag;
2008-04-13 wenzelm Sorts.class_error: produce message only (formerly msg_class_error);
2008-04-13 wenzelm tsig: removed unnecessary universal witness;
2008-04-13 wenzelm simplified handling of sorts, removed unnecessary universal witness;
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;
(0) -10000 -3000 -1000 -300 -100 -50 -24 +24 +50 +100 +300 +1000 +3000 +10000 +30000 tip