src/Pure/meta_simplifier.ML
Tue, 04 Oct 2005 19:01:37 +0200 wenzelm minor tweaks for Poplog/ML;
Thu, 29 Sep 2005 15:50:46 +0200 wenzelm export debug_bounds;
Thu, 29 Sep 2005 12:33:26 +0200 berghofe Simplifier now removes flex-flex constraints from theorem returned by prover.
Thu, 29 Sep 2005 00:58:58 +0200 wenzelm removed revert_bound;
Fri, 23 Sep 2005 22:21:54 +0200 wenzelm added mk_solver';
Tue, 20 Sep 2005 08:21:49 +0200 haftmann slight adaptions to library changes
Fri, 02 Sep 2005 15:54:47 +0200 haftmann some 'assoc' etc. refactoring
Wed, 31 Aug 2005 15:46:40 +0200 wenzelm refer to theory instead of low-level tsig;
Tue, 16 Aug 2005 12:51:07 +0200 nipkow simp_depth warning now mod 20, not mod 10 (too often)
Mon, 01 Aug 2005 19:20:39 +0200 wenzelm improved bounds: nameless Term.bound, recover names for output;
Thu, 28 Jul 2005 15:19:55 +0200 wenzelm Term.bound;
Fri, 15 Jul 2005 15:44:15 +0200 wenzelm tuned fold on terms;
Thu, 14 Jul 2005 19:28:24 +0200 wenzelm tuned;
Wed, 13 Jul 2005 16:07:28 +0200 wenzelm export eq_rrule;
Fri, 01 Jul 2005 22:33:59 +0200 wenzelm decomp_simp: compare terms, not cterms;
Fri, 17 Jun 2005 18:35:27 +0200 wenzelm accomodate change of TheoryDataFun;
Mon, 13 Jun 2005 13:10:45 +0200 nipkow changed -1 back to 0
Sun, 12 Jun 2005 08:53:41 +0200 nipkow simp_depth now starts at -1 to make it start at 0 ;-)
Mon, 06 Jun 2005 19:09:49 +0200 nipkow Added the t = x "fix" - in (* ... *) :-(
Mon, 23 May 2005 11:14:58 +0200 nipkow tuned trace info (depth)
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Mon, 24 Jan 2005 18:11:06 +0100 berghofe Removed unnecessary subsignature checks to speed up rewriting.
Mon, 18 Oct 2004 11:43:40 +0200 berghofe Replaced list of bound variables in simpset by maximal index of bound
Sat, 11 Sep 2004 18:35:43 +0200 nipkow undoing previous change
Fri, 10 Sep 2004 00:19:15 +0200 nipkow new forward deduction capability for simplifier
Fri, 30 Jul 2004 10:41:52 +0200 wenzelm tuned output;
Sun, 11 Jul 2004 20:34:50 +0200 wenzelm improved print_ss; tuned;
Thu, 08 Jul 2004 19:33:51 +0200 wenzelm major cleanup; got rid of obsolete meta_simpset;
Wed, 30 Jun 2004 00:42:59 +0200 skalberg Made simplification procedures simpset-aware.
Fri, 25 Jun 2004 14:30:55 +0200 skalberg Merging the meta-simplifier with the Provers-simplifier. Next step:
Wed, 23 Jun 2004 14:44:22 +0200 skalberg Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Thu, 22 Apr 2004 10:52:32 +0200 wenzelm tuned;
Thu, 25 Dec 2003 23:18:04 +0100 nipkow Added trace msg
Tue, 21 Oct 2003 11:09:23 +0200 skalberg Added access to the mk_rews field (and friends).
Tue, 20 May 2003 11:52:42 +0200 kleing be less verbose about simplification depth
Mon, 28 Apr 2003 12:01:45 +0200 ballarin Simplifier no longer aborts on failed congruence proof.
Thu, 27 Feb 2003 15:12:29 +0100 ballarin Change to meta simplifier: congruence rules may now have frees as head of term.
Tue, 25 Feb 2003 18:49:23 +0100 nipkow added simp_depth_limit
Mon, 21 Oct 2002 17:09:31 +0200 berghofe No more explicit manipulation of flex-flex constraints in goals_conv.
Tue, 01 Oct 2002 11:17:25 +0200 berghofe Deleted superfluous dest_implies.
Mon, 30 Sep 2002 16:38:22 +0200 berghofe Completely reimplemented mutual simplification of premises.
Thu, 19 Sep 2002 16:01:29 +0200 nipkow drule: added nRS
Thu, 08 Aug 2002 23:51:24 +0200 wenzelm exception SIMPROC_FAIL: solid error reporting of simprocs;
Mon, 05 Aug 2002 21:17:45 +0200 wenzelm protect simplifier operation against spurious exceptions from simprocs;
Fri, 31 May 2002 18:48:31 +0200 berghofe Changed interface of rewrite_term.
Thu, 28 Feb 2002 19:22:56 +0100 wenzelm decomp_simp': use lhs instead of elhs (preserves more bound variable names);
Wed, 16 Jan 2002 23:17:44 +0100 wenzelm interface to Pattern.rewrite_term;
Wed, 16 Jan 2002 20:58:27 +0100 wenzelm export beta_eta_conversion;
Thu, 27 Dec 2001 16:46:52 +0100 wenzelm tuned tracing markup;
Sat, 24 Nov 2001 16:56:26 +0100 wenzelm gen_merge_lists;
Wed, 21 Nov 2001 00:36:51 +0100 wenzelm use tracing function for trace output;
Mon, 12 Nov 2001 10:44:55 +0100 berghofe congc now returns None if congruence rule has no effect.
Mon, 22 Oct 2001 18:01:38 +0200 wenzelm Display.pretty_thms;
Sun, 14 Oct 2001 22:05:01 +0200 wenzelm tuned rewrite/simplify interface;
Sun, 14 Oct 2001 20:08:11 +0200 wenzelm tuned;
Fri, 12 Oct 2001 18:29:51 +0200 berghofe Tuned comment.
Fri, 12 Oct 2001 16:57:07 +0200 berghofe - Exported goals_conv and fconv_rule
less more (0) -60 tip