src/Sequents/simpdata.ML
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Wed, 11 Jan 2012 16:25:34 +0100 wenzelm more qualified names;
Mon, 28 Nov 2011 17:05:41 +0100 wenzelm avoid stepping outside of context -- plain zero_var_indexes should be sufficient;
Thu, 24 Nov 2011 21:01:06 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Wed, 23 Nov 2011 22:59:39 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Wed, 29 Jun 2011 21:34:16 +0200 wenzelm tuned signature;
Wed, 29 Jun 2011 20:39:41 +0200 wenzelm simplified/unified Simplifier.mk_solver;
Fri, 13 May 2011 23:58:40 +0200 wenzelm clarified map_simpset versus Simplifier.map_simpset_global;
Tue, 17 Aug 2010 19:36:39 +0200 haftmann more antiquotations
Fri, 30 Apr 2010 18:06:29 +0200 wenzelm proper context for rule_by_tactic;
Thu, 29 Apr 2010 22:56:32 +0200 wenzelm proper context for mksimps etc. -- via simpset of the running Simplifier;
Sat, 13 Mar 2010 16:44:12 +0100 wenzelm removed old CVS Ids;
Fri, 19 Feb 2010 16:11:45 +0100 wenzelm renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Sat, 17 Oct 2009 00:52:37 +0200 wenzelm explicitly qualify Drule.standard;
Thu, 23 Jul 2009 23:12:21 +0200 wenzelm more @{theory} antiquotations;
Tue, 21 Jul 2009 01:03:18 +0200 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
Wed, 11 Jun 2008 15:41:33 +0200 wenzelm converted ML proofs from simpdata.ML;
Sat, 17 May 2008 13:54:30 +0200 wenzelm structure Display: less pervasive operations;
Wed, 09 May 2007 19:37:21 +0200 wenzelm tuned ML setup;
Tue, 21 Nov 2006 00:07:05 +0100 wenzelm removed legacy ML setup;
Mon, 20 Nov 2006 23:47:10 +0100 wenzelm converted legacy ML scripts;
Tue, 18 Oct 2005 17:59:25 +0200 wenzelm Simplifier.theory_context;
Mon, 17 Oct 2005 23:10:13 +0200 wenzelm change_claset/simpset;
Sun, 18 Sep 2005 15:20:08 +0200 wenzelm converted to Isar theory format;
Sat, 12 Jan 2002 16:37:58 +0100 wenzelm renamed forall_elim_vars_safe to gen_all;
Fri, 11 Jan 2002 14:53:30 +0100 wenzelm replace gen_all by forall_elim_vars_safe;
Tue, 29 Aug 2000 00:55:31 +0200 wenzelm cong setup now part of Simplifier;
Thu, 06 Jul 2000 11:24:09 +0200 paulson removal of batch style, and tidying
Tue, 21 Sep 1999 19:11:07 +0200 nipkow Mod because of new solver interface.
Wed, 28 Jul 1999 13:55:34 +0200 paulson congruence rule for |-, etc.
Tue, 27 Jul 1999 19:02:43 +0200 paulson installation of simplifier and classical reasoner, better rules etc
less more (0) tip