2008-04-13 ago wenzelm tsig: removed unnecessary universal witness;
2008-04-13 ago wenzelm tuned;
2008-04-12 ago wenzelm removed unnecessary Goal.close_result;
2008-04-12 ago wenzelm replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2008-04-12 ago wenzelm advance: do not count utf8 trailer bytes (which happen to be undefined or punctuation in iso-latin);
2008-04-12 ago wenzelm added is_utf8_trailer;
2008-04-12 ago wenzelm rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-12 ago wenzelm obsolete -- Poly/ML images are maximally shared already, home-grown compression wastes space and time;
2008-04-12 ago wenzelm removed obsolete compress.ML
2008-04-12 ago wenzelm replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2008-04-12 ago wenzelm rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-12 ago wenzelm rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-10 ago wenzelm use_text: explicitly print exception, which is no longer done by the new PolyML.compiler setup;
2008-04-10 ago wenzelm transaction/init: ensure stable theory (non-draft);
2008-04-10 ago wenzelm export is_draft, not draftN;
2008-04-10 ago wenzelm simplified isarcmd;
2008-04-10 ago wenzelm eliminated unused name_of, source, source_of, print', print3, three_buffersN;
2008-04-10 ago wenzelm eliminated unused trace, read;
2008-04-10 ago wenzelm eliminated unused Toplevel.print3/three_buffers;
2008-04-10 ago wenzelm tuned;
2008-04-10 ago wenzelm Isar.goal: tactical goal only;
2008-04-10 ago wenzelm eliminated backpatching of load_thy;
2008-04-10 ago wenzelm added read_const_exprs (from Pure/Isar/code_unit.ML);
2008-04-10 ago wenzelm export get_names (formerly names);
2008-04-10 ago wenzelm ThyInfo.get_names;
2008-04-10 ago wenzelm ThyInfo.get_theory;
2008-04-10 ago wenzelm export load_thy -- no backpatching;
2008-04-10 ago wenzelm export subst_alias;
2008-04-10 ago wenzelm load thy_info.ML after outer_syntax.ML -- avoids backpatching of load_thy;
2008-04-10 ago wenzelm val theory = ThyInfo.get_theory;
2008-04-10 ago wenzelm replaced Isar loop variants by generic toplevel_loop;
2008-04-10 ago wenzelm replaced Isar loop variants by generic toplevel_loop;
2008-04-10 ago wenzelm The global Isabelle/Isar state and main read-eval-print loop.
2008-04-10 ago wenzelm replaced Isar.toplevel by Toplevel.program;
2008-04-10 ago wenzelm moved global Toplevel state to structure Isar;
2008-04-10 ago wenzelm made purely value-oriented, moved global state to structure Isar (cf. isar.ML);
2008-04-10 ago wenzelm finish: removed unnecessary Isar.init;
2008-04-10 ago wenzelm moved structure Isar to isar.ML;
2008-04-10 ago wenzelm Context.set_thread_data: non-critical;
2008-04-10 ago wenzelm added Isar/isar.ML;
2008-04-10 ago haftmann improvements are strict
2008-04-10 ago haftmann check validity of class target improvement
2008-04-09 ago wenzelm print_consts only for external specifications;
2008-04-09 ago wenzelm fundef_afterqed: removed unused config, added do_print flag;
2008-04-09 ago wenzelm minimal error handling;
2008-04-09 ago wenzelm replaced ML by ML_val;
2008-04-09 ago wenzelm avoid control symbols in document (\<^fixed>);
2008-04-09 ago wenzelm \usepackage[english]{babel} (required for guillemots);
2008-04-09 ago haftmann renamed mbind to scomp
2008-04-09 ago haftmann removed syntax from monad combinators; renamed mbind to scomp
2008-04-09 ago haftmann rudimentary user-syntax for terms
2008-04-09 ago huffman fix spelling
2008-04-09 ago huffman fix spelling
2008-04-09 ago huffman move lemmas from Word/BinBoolList.thy to List.thy
2008-04-08 ago krauss fixed makefiles
2008-04-08 ago krauss added missing file
2008-04-08 ago wenzelm tuned;
2008-04-08 ago krauss Generic conversion and tactic "atomize_elim" to convert elimination rules
2008-04-08 ago wenzelm obsolete;
2008-04-08 ago wenzelm removed isatool expandshort;