src/Sequents/simpdata.ML
2012-01-11 wenzelm more qualified names;
2011-11-28 wenzelm avoid stepping outside of context -- plain zero_var_indexes should be sufficient;
2011-11-24 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-11-23 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-06-29 wenzelm tuned signature;
2011-06-29 wenzelm simplified/unified Simplifier.mk_solver;
2011-05-13 wenzelm clarified map_simpset versus Simplifier.map_simpset_global;
2010-08-17 haftmann more antiquotations
2010-04-30 wenzelm proper context for rule_by_tactic;
2010-04-29 wenzelm proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-03-13 wenzelm removed old CVS Ids;
2010-02-19 wenzelm renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2010-02-07 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-10-16 wenzelm explicitly qualify Drule.standard;
2009-07-23 wenzelm more @{theory} antiquotations;
2009-07-20 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2008-06-11 wenzelm converted ML proofs from simpdata.ML;
2008-05-17 wenzelm structure Display: less pervasive operations;
2007-05-09 wenzelm tuned ML setup;
2006-11-20 wenzelm removed legacy ML setup;
2006-11-20 wenzelm converted legacy ML scripts;
2005-10-18 wenzelm Simplifier.theory_context;
2005-10-17 wenzelm change_claset/simpset;
2005-09-18 wenzelm converted to Isar theory format;
2002-01-12 wenzelm renamed forall_elim_vars_safe to gen_all;
2002-01-11 wenzelm replace gen_all by forall_elim_vars_safe;
2000-08-28 wenzelm cong setup now part of Simplifier;
2000-07-06 paulson removal of batch style, and tidying
1999-09-21 nipkow Mod because of new solver interface.
1999-07-28 paulson congruence rule for |-, etc.
less more (0) tip