src/HOL/Import/shuffler.ML
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-08-28 wenzelm 2009-08-28 modernized messages -- eliminated ctyp/cterm operations;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-06 wenzelm 2009-07-06 structure Thm: less pervasive names;
2009-05-27 wenzelm 2009-05-27 fixed superficial ML lapses introduced in b3c7044d47b6;
2009-05-25 wenzelm 2009-05-25 modernized method setup; tuned signature;
2009-03-15 wenzelm 2009-03-15 simplified attribute setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-12 wenzelm 2009-03-12 Assumption.all_prems_of, Assumption.all_assms_of;
2009-01-01 wenzelm 2009-01-01 eliminated OldTerm.(add_)term_consts;
2008-12-31 wenzelm 2008-12-31 eliminated OldTerm.add_term_free_names;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-09-29 wenzelm 2008-09-29 handle _ should be avoided (spurious Interrupt will spoil the game);
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-06-23 wenzelm 2008-06-23 Logic.all/mk_equals/mk_implies;
2008-06-12 wenzelm 2008-06-12 Facts.dest/export_static: content difference;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-04-16 wenzelm 2008-04-16 Facts.dest_static;
2008-04-15 wenzelm 2008-04-15 Facts.dest_table;
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure;
2008-03-15 wenzelm 2008-03-15 removed obsolete PureThy.thms_containing_consts;
2007-09-18 wenzelm 2007-09-18 simplified PrintMode interfaces;
2007-05-10 wenzelm 2007-05-10 moved some Drule operations to Thm (see more_thm.ML);
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2006-10-20 haftmann 2006-10-20 slight cleanup
2006-10-10 haftmann 2006-10-10 gen_rem(s) abandoned in favour of remove / subtract
2006-10-09 wenzelm 2006-10-09 attribute: Context.mapping;
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-08-03 obua 2006-08-03 fixed generator
2006-07-27 wenzelm 2006-07-27 moved basic assumption operations from structure ProofContext to Assumption;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-07-04 wenzelm 2006-07-04 Thm.varifyT;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-11-09 wenzelm 2005-11-09 Thm.varifyT': natural argument order;
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-10-18 wenzelm 2005-10-18 Simplifier.theory_context;
2005-09-17 wenzelm 2005-09-17 removed spurious PolyML.exception_trace;
2005-09-16 obua 2005-09-16 fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
2005-08-29 obua 2005-08-29 Updated import.
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; Context.str_of_thy;
2005-04-21 berghofe 2005-04-21 Adapted to new interface of instantiation and unification / matching functions.
2005-04-07 wenzelm 2005-04-07 reverted renaming of Some/None in comments and strings;
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2004-05-31 wenzelm 2004-05-31 oops -- no Output.out here;
2004-05-29 wenzelm 2004-05-29 Output.output;
2004-04-17 skalberg 2004-04-17 Minor cleanup of headers and some speedup of the HOL4 import.
2004-04-04 skalberg 2004-04-04 Added a number of explicit type casts and delayed evaluations (all seemingly needless) so that SML/NJ 110.9.1 would accept the importer...
2004-04-02 skalberg 2004-04-02 Added HOL proof importer.