src/Pure/meta_simplifier.ML
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
Fri, 30 Apr 2010 17:18:29 +0200 wenzelm conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context;
Thu, 29 Apr 2010 22:56:32 +0200 wenzelm proper context for mksimps etc. -- via simpset of the running Simplifier;
Mon, 26 Apr 2010 20:30:50 +0200 wenzelm eliminanated some unreferenced identifiers;
Mon, 29 Mar 2010 09:06:34 +0200 boehmes the configuration option 'trace_simp' now uses the reference of the ProofGeneral settings menu as (dynamic) default value
Sun, 28 Mar 2010 16:59:06 +0200 wenzelm static defaults for configuration options;
Sat, 27 Mar 2010 21:34:28 +0100 boehmes re-introduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)
Fri, 26 Mar 2010 23:46:22 +0100 boehmes replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
Sat, 20 Mar 2010 17:33:11 +0100 wenzelm renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
Sat, 27 Feb 2010 23:13:01 +0100 wenzelm modernized structure Term_Ord;
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;
Fri, 19 Feb 2010 11:56:11 +0100 wenzelm tuned message;
Wed, 25 Nov 2009 09:13:46 +0100 haftmann normalized uncurry take/drop
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Sun, 08 Nov 2009 18:42:57 +0100 wenzelm tuned;
Mon, 02 Nov 2009 17:29:48 +0100 wenzelm back to warning -- Proof General tends to "popup" tracing output;
Thu, 29 Oct 2009 20:53:24 +0100 wenzelm less aggressive tracing;
Tue, 27 Oct 2009 22:56:14 +0100 wenzelm eliminated some old folds;
Wed, 21 Oct 2009 08:16:25 +0200 haftmann merged
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Tue, 20 Oct 2009 16:13:01 +0200 haftmann replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
Tue, 20 Oct 2009 21:26:45 +0200 wenzelm backpatching of structure Proof and ProofContext -- avoid odd aliases;
Tue, 20 Oct 2009 20:54:31 +0200 wenzelm uniform use of Integer.min/max;
Wed, 30 Sep 2009 23:49:53 +0200 wenzelm eliminated dead code;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Sat, 30 May 2009 11:57:36 +0200 wenzelm tuned;
Tue, 21 Apr 2009 09:53:27 +0200 krauss replace type cong = {thm : thm, lhs : term} by plain thm -- the other component has been unused for a long time.
Mon, 16 Mar 2009 23:36:55 +0100 wenzelm provide Simplifier.norm_hhf(_protect) as regular simplifier operation;
Sun, 08 Mar 2009 12:15:58 +0100 wenzelm added dest_ss;
Sat, 07 Mar 2009 11:45:56 +0100 wenzelm renamed rep_ss to MetaSimplifier.internal_ss;
Fri, 06 Mar 2009 22:32:27 +0100 wenzelm replaced archaic use of rep_ss by Simplifier.mksimps;
Wed, 31 Dec 2008 15:30:10 +0100 wenzelm moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
Tue, 18 Nov 2008 18:25:42 +0100 wenzelm eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
Thu, 16 Oct 2008 22:44:29 +0200 wenzelm Drule.norm_hhf_eqs;
Thu, 14 Aug 2008 16:52:46 +0200 wenzelm moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
Mon, 14 Jul 2008 19:20:57 +0200 haftmann dropped junk
Mon, 14 Jul 2008 11:04:47 +0200 haftmann added further simple interfaces
Sat, 21 Jun 2008 16:18:49 +0200 wenzelm activate_context: strict the_context, no fallback on theory context;
Thu, 29 May 2008 23:46:45 +0200 wenzelm legacy_feature: no proof context in simpset;
Sun, 18 May 2008 15:04:09 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Sat, 12 Apr 2008 17:00:35 +0200 wenzelm rep_cterm/rep_thm: no longer dereference theory_ref;
Thu, 27 Mar 2008 14:41:09 +0100 wenzelm eliminated theory ProtoPure;
Tue, 27 Nov 2007 15:47:40 +0100 berghofe check_conv now only performs beta-eta-normalization when equations
Fri, 26 Oct 2007 17:55:33 +0200 wenzelm asm_rewrite_goal_tac: avoiding PRIMITIVE lets informative exceptions (from simprocs) get through;
Tue, 25 Sep 2007 13:28:37 +0200 wenzelm Syntax.parse/check/read;
Mon, 20 Aug 2007 20:43:58 +0200 wenzelm tuned merge operations via pointer_eq;
Thu, 02 Aug 2007 12:06:27 +0200 wenzelm turned simp_depth_limit into configuration option;
Mon, 23 Jul 2007 19:45:45 +0200 wenzelm depth flag: plain bool ref;
Thu, 05 Jul 2007 20:01:35 +0200 wenzelm tuned;
Thu, 05 Jul 2007 00:06:23 +0200 wenzelm tuned goal conversion interfaces;
Tue, 03 Jul 2007 17:17:11 +0200 wenzelm moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
Sun, 03 Jun 2007 23:16:49 +0200 wenzelm merge_ss: plain merge of prems;
Thu, 31 May 2007 23:47:36 +0200 wenzelm simplified/unified list fold;
Thu, 10 May 2007 00:39:48 +0200 wenzelm moved some Drule operations to Thm (see more_thm.ML);
Wed, 09 May 2007 19:20:00 +0200 wenzelm simp_depth: now proper value in simpset (prevents problems with lost exception trace, enables multi-threaded simplification);
Mon, 16 Apr 2007 16:11:03 +0200 haftmann canonical merge operations
Sat, 14 Apr 2007 00:46:20 +0200 wenzelm Morphism.transform/form;
Mon, 26 Feb 2007 23:18:24 +0100 wenzelm moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
Tue, 06 Feb 2007 19:32:31 +0100 wenzelm trace/debug: avoid eager string concatenation;
Sun, 04 Feb 2007 22:02:14 +0100 wenzelm type simproc: explicitl dependency of morphism;
Wed, 31 Jan 2007 16:05:14 +0100 haftmann changed cong alist - now using AList operations instead of overwrite_warn
Thu, 04 Jan 2007 21:18:05 +0100 wenzelm added mk_simproc': tuned interface;
Sat, 30 Dec 2006 16:08:00 +0100 wenzelm removed conditional combinator;
Thu, 07 Dec 2006 23:16:55 +0100 wenzelm reorganized structure Tactic vs. MetaSimplifier;
Tue, 05 Dec 2006 00:30:38 +0100 wenzelm thm/prf: separate official name vs. additional tags;
Thu, 30 Nov 2006 14:17:29 +0100 wenzelm qualified MetaSimplifier.norm_hhf(_protect);
Wed, 29 Nov 2006 04:11:09 +0100 wenzelm simplified Logic.count_prems;
Tue, 28 Nov 2006 00:35:18 +0100 wenzelm simplified '?' operator;
Fri, 24 Nov 2006 22:05:12 +0100 wenzelm ProofContext.init;
Fri, 10 Nov 2006 07:44:47 +0100 haftmann introduces canonical AList functions for loop_tacs
Wed, 11 Oct 2006 10:49:36 +0200 haftmann abandoned findrep
Mon, 09 Oct 2006 02:19:57 +0200 wenzelm Drule.lhs/rhs_of;
Thu, 21 Sep 2006 19:05:08 +0200 wenzelm member (op =);
Mon, 18 Sep 2006 19:39:07 +0200 wenzelm Thm.dest_arg;
Fri, 15 Sep 2006 20:08:38 +0200 wenzelm rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
Thu, 03 Aug 2006 17:30:38 +0200 wenzelm tuned;
Wed, 02 Aug 2006 22:26:41 +0200 wenzelm normalized Proof.context/method type aliases;
Sun, 30 Jul 2006 21:28:52 +0200 wenzelm Thm.adjust_maxidx;
Thu, 27 Jul 2006 13:43:06 +0200 wenzelm moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);
Tue, 25 Jul 2006 21:18:04 +0200 wenzelm use Term.add_vars instead of obsolete term_varnames;
Tue, 18 Jul 2006 20:01:41 +0200 wenzelm Term.declare_term_names;
Tue, 11 Jul 2006 12:17:04 +0200 wenzelm replaced Term.variant(list) by Name.variant(_list);
Sat, 08 Jul 2006 12:54:45 +0200 wenzelm tuned exception handling;
Thu, 06 Jul 2006 16:49:40 +0200 wenzelm add/del_simps: warning for inactive simpset (no context);
Tue, 06 Jun 2006 20:42:28 +0200 wenzelm tuned;
Thu, 11 May 2006 19:19:33 +0200 wenzelm tuned;
Sat, 29 Apr 2006 23:16:43 +0200 wenzelm tuned;
Thu, 27 Apr 2006 15:06:35 +0200 wenzelm tuned basic list operators (flat, maps, map_filter);
Tue, 21 Mar 2006 12:18:11 +0100 wenzelm gen_eq_set, remove (op =);
Sun, 26 Feb 2006 23:01:48 +0100 wenzelm rewrite_goals_rule_aux: actually use prems if present;
Wed, 15 Feb 2006 21:35:02 +0100 wenzelm rewrite_cterm: Thm.adjust_maxidx prevents unnecessary increments on rules;
Mon, 06 Feb 2006 20:58:54 +0100 wenzelm Envir.(beta_)eta_contract;
Wed, 04 Jan 2006 16:38:40 +0100 nipkow trace_simp_depth_limit is 1 by default
Thu, 22 Dec 2005 00:29:00 +0100 wenzelm renamed imp_cong' to imp_cong_rule;
Sat, 19 Nov 2005 14:21:05 +0100 wenzelm simpset: added reorient field, set_reorient;
Fri, 21 Oct 2005 18:14:46 +0200 wenzelm moved various simplification tactics and rules to simplifier.ML;
Tue, 18 Oct 2005 17:59:30 +0200 wenzelm renamed set_context to context;
Mon, 17 Oct 2005 23:10:20 +0200 wenzelm added set/addloop' for simpset dependent loopers;
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.
less more (0) -120 tip