| Tue, 25 Sep 2007 13:28:37 +0200 |
wenzelm |
Syntax.parse/check/read;
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 20:43:58 +0200 |
wenzelm |
tuned merge operations via pointer_eq;
|
file |
diff |
annotate
|
| Thu, 02 Aug 2007 12:06:27 +0200 |
wenzelm |
turned simp_depth_limit into configuration option;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 19:45:45 +0200 |
wenzelm |
depth flag: plain bool ref;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 20:01:35 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 00:06:23 +0200 |
wenzelm |
tuned goal conversion interfaces;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Sun, 03 Jun 2007 23:16:49 +0200 |
wenzelm |
merge_ss: plain merge of prems;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 23:47:36 +0200 |
wenzelm |
simplified/unified list fold;
|
file |
diff |
annotate
|
| Thu, 10 May 2007 00:39:48 +0200 |
wenzelm |
moved some Drule operations to Thm (see more_thm.ML);
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Mon, 16 Apr 2007 16:11:03 +0200 |
haftmann |
canonical merge operations
|
file |
diff |
annotate
|
| Sat, 14 Apr 2007 00:46:20 +0200 |
wenzelm |
Morphism.transform/form;
|
file |
diff |
annotate
|
| Mon, 26 Feb 2007 23:18:24 +0100 |
wenzelm |
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
|
file |
diff |
annotate
|
| Tue, 06 Feb 2007 19:32:31 +0100 |
wenzelm |
trace/debug: avoid eager string concatenation;
|
file |
diff |
annotate
|
| Sun, 04 Feb 2007 22:02:14 +0100 |
wenzelm |
type simproc: explicitl dependency of morphism;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2007 16:05:14 +0100 |
haftmann |
changed cong alist - now using AList operations instead of overwrite_warn
|
file |
diff |
annotate
|
| Thu, 04 Jan 2007 21:18:05 +0100 |
wenzelm |
added mk_simproc': tuned interface;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2006 16:08:00 +0100 |
wenzelm |
removed conditional combinator;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 23:16:55 +0100 |
wenzelm |
reorganized structure Tactic vs. MetaSimplifier;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 00:30:38 +0100 |
wenzelm |
thm/prf: separate official name vs. additional tags;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 14:17:29 +0100 |
wenzelm |
qualified MetaSimplifier.norm_hhf(_protect);
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 04:11:09 +0100 |
wenzelm |
simplified Logic.count_prems;
|
file |
diff |
annotate
|
| Tue, 28 Nov 2006 00:35:18 +0100 |
wenzelm |
simplified '?' operator;
|
file |
diff |
annotate
|
| Fri, 24 Nov 2006 22:05:12 +0100 |
wenzelm |
ProofContext.init;
|
file |
diff |
annotate
|
| Fri, 10 Nov 2006 07:44:47 +0100 |
haftmann |
introduces canonical AList functions for loop_tacs
|
file |
diff |
annotate
|
| Wed, 11 Oct 2006 10:49:36 +0200 |
haftmann |
abandoned findrep
|
file |
diff |
annotate
|
| Mon, 09 Oct 2006 02:19:57 +0200 |
wenzelm |
Drule.lhs/rhs_of;
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 19:05:08 +0200 |
wenzelm |
member (op =);
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 19:39:07 +0200 |
wenzelm |
Thm.dest_arg;
|
file |
diff |
annotate
|
| Fri, 15 Sep 2006 20:08:38 +0200 |
wenzelm |
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 17:30:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:41 +0200 |
wenzelm |
normalized Proof.context/method type aliases;
|
file |
diff |
annotate
|
| Sun, 30 Jul 2006 21:28:52 +0200 |
wenzelm |
Thm.adjust_maxidx;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 13:43:06 +0200 |
wenzelm |
moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);
|
file |
diff |
annotate
|
| Tue, 25 Jul 2006 21:18:04 +0200 |
wenzelm |
use Term.add_vars instead of obsolete term_varnames;
|
file |
diff |
annotate
|
| Tue, 18 Jul 2006 20:01:41 +0200 |
wenzelm |
Term.declare_term_names;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:17:04 +0200 |
wenzelm |
replaced Term.variant(list) by Name.variant(_list);
|
file |
diff |
annotate
|
| Sat, 08 Jul 2006 12:54:45 +0200 |
wenzelm |
tuned exception handling;
|
file |
diff |
annotate
|
| Thu, 06 Jul 2006 16:49:40 +0200 |
wenzelm |
add/del_simps: warning for inactive simpset (no context);
|
file |
diff |
annotate
|
| Tue, 06 Jun 2006 20:42:28 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 11 May 2006 19:19:33 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 29 Apr 2006 23:16:43 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Tue, 21 Mar 2006 12:18:11 +0100 |
wenzelm |
gen_eq_set, remove (op =);
|
file |
diff |
annotate
|
| Sun, 26 Feb 2006 23:01:48 +0100 |
wenzelm |
rewrite_goals_rule_aux: actually use prems if present;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:35:02 +0100 |
wenzelm |
rewrite_cterm: Thm.adjust_maxidx prevents unnecessary increments on rules;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:58:54 +0100 |
wenzelm |
Envir.(beta_)eta_contract;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2006 16:38:40 +0100 |
nipkow |
trace_simp_depth_limit is 1 by default
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:29:00 +0100 |
wenzelm |
renamed imp_cong' to imp_cong_rule;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2005 14:21:05 +0100 |
wenzelm |
simpset: added reorient field, set_reorient;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:14:46 +0200 |
wenzelm |
moved various simplification tactics and rules to simplifier.ML;
|
file |
diff |
annotate
|
| Tue, 18 Oct 2005 17:59:30 +0200 |
wenzelm |
renamed set_context to context;
|
file |
diff |
annotate
|
| Mon, 17 Oct 2005 23:10:20 +0200 |
wenzelm |
added set/addloop' for simpset dependent loopers;
|
file |
diff |
annotate
|
| Tue, 04 Oct 2005 19:01:37 +0200 |
wenzelm |
minor tweaks for Poplog/ML;
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 15:50:46 +0200 |
wenzelm |
export debug_bounds;
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 12:33:26 +0200 |
berghofe |
Simplifier now removes flex-flex constraints from theorem returned by prover.
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 00:58:58 +0200 |
wenzelm |
removed revert_bound;
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 22:21:54 +0200 |
wenzelm |
added mk_solver';
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 08:21:49 +0200 |
haftmann |
slight adaptions to library changes
|
file |
diff |
annotate
|
| Fri, 02 Sep 2005 15:54:47 +0200 |
haftmann |
some 'assoc' etc. refactoring
|
file |
diff |
annotate
|
| Wed, 31 Aug 2005 15:46:40 +0200 |
wenzelm |
refer to theory instead of low-level tsig;
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 12:51:07 +0200 |
nipkow |
simp_depth warning now mod 20, not mod 10 (too often)
|
file |
diff |
annotate
|
| Mon, 01 Aug 2005 19:20:39 +0200 |
wenzelm |
improved bounds: nameless Term.bound, recover names for output;
|
file |
diff |
annotate
|
| Thu, 28 Jul 2005 15:19:55 +0200 |
wenzelm |
Term.bound;
|
file |
diff |
annotate
|
| Fri, 15 Jul 2005 15:44:15 +0200 |
wenzelm |
tuned fold on terms;
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 19:28:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 16:07:28 +0200 |
wenzelm |
export eq_rrule;
|
file |
diff |
annotate
|
| Fri, 01 Jul 2005 22:33:59 +0200 |
wenzelm |
decomp_simp: compare terms, not cterms;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:35:27 +0200 |
wenzelm |
accomodate change of TheoryDataFun;
|
file |
diff |
annotate
|
| Mon, 13 Jun 2005 13:10:45 +0200 |
nipkow |
changed -1 back to 0
|
file |
diff |
annotate
|
| Sun, 12 Jun 2005 08:53:41 +0200 |
nipkow |
simp_depth now starts at -1 to make it start at 0 ;-)
|
file |
diff |
annotate
|
| Mon, 06 Jun 2005 19:09:49 +0200 |
nipkow |
Added the t = x "fix" - in (* ... *) :-(
|
file |
diff |
annotate
|
| Mon, 23 May 2005 11:14:58 +0200 |
nipkow |
tuned trace info (depth)
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Mon, 24 Jan 2005 18:11:06 +0100 |
berghofe |
Removed unnecessary subsignature checks to speed up rewriting.
|
file |
diff |
annotate
|
| Mon, 18 Oct 2004 11:43:40 +0200 |
berghofe |
Replaced list of bound variables in simpset by maximal index of bound
|
file |
diff |
annotate
|
| Sat, 11 Sep 2004 18:35:43 +0200 |
nipkow |
undoing previous change
|
file |
diff |
annotate
|
| Fri, 10 Sep 2004 00:19:15 +0200 |
nipkow |
new forward deduction capability for simplifier
|
file |
diff |
annotate
|
| Fri, 30 Jul 2004 10:41:52 +0200 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Sun, 11 Jul 2004 20:34:50 +0200 |
wenzelm |
improved print_ss; tuned;
|
file |
diff |
annotate
|
| Thu, 08 Jul 2004 19:33:51 +0200 |
wenzelm |
major cleanup; got rid of obsolete meta_simpset;
|
file |
diff |
annotate
|
| Wed, 30 Jun 2004 00:42:59 +0200 |
skalberg |
Made simplification procedures simpset-aware.
|
file |
diff |
annotate
|
| Fri, 25 Jun 2004 14:30:55 +0200 |
skalberg |
Merging the meta-simplifier with the Provers-simplifier. Next step:
|
file |
diff |
annotate
|
| Wed, 23 Jun 2004 14:44:22 +0200 |
skalberg |
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Thu, 22 Apr 2004 10:52:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 25 Dec 2003 23:18:04 +0100 |
nipkow |
Added trace msg
|
file |
diff |
annotate
|
| Tue, 21 Oct 2003 11:09:23 +0200 |
skalberg |
Added access to the mk_rews field (and friends).
|
file |
diff |
annotate
|
| Tue, 20 May 2003 11:52:42 +0200 |
kleing |
be less verbose about simplification depth
|
file |
diff |
annotate
|
| Mon, 28 Apr 2003 12:01:45 +0200 |
ballarin |
Simplifier no longer aborts on failed congruence proof.
|
file |
diff |
annotate
|
| Thu, 27 Feb 2003 15:12:29 +0100 |
ballarin |
Change to meta simplifier: congruence rules may now have frees as head of term.
|
file |
diff |
annotate
|
| Tue, 25 Feb 2003 18:49:23 +0100 |
nipkow |
added simp_depth_limit
|
file |
diff |
annotate
|
| Mon, 21 Oct 2002 17:09:31 +0200 |
berghofe |
No more explicit manipulation of flex-flex constraints in goals_conv.
|
file |
diff |
annotate
|
| Tue, 01 Oct 2002 11:17:25 +0200 |
berghofe |
Deleted superfluous dest_implies.
|
file |
diff |
annotate
|
| Mon, 30 Sep 2002 16:38:22 +0200 |
berghofe |
Completely reimplemented mutual simplification of premises.
|
file |
diff |
annotate
|
| Thu, 19 Sep 2002 16:01:29 +0200 |
nipkow |
drule: added nRS
|
file |
diff |
annotate
|
| Thu, 08 Aug 2002 23:51:24 +0200 |
wenzelm |
exception SIMPROC_FAIL: solid error reporting of simprocs;
|
file |
diff |
annotate
|
| Mon, 05 Aug 2002 21:17:45 +0200 |
wenzelm |
protect simplifier operation against spurious exceptions from simprocs;
|
file |
diff |
annotate
|
| Fri, 31 May 2002 18:48:31 +0200 |
berghofe |
Changed interface of rewrite_term.
|
file |
diff |
annotate
|
| Thu, 28 Feb 2002 19:22:56 +0100 |
wenzelm |
decomp_simp': use lhs instead of elhs (preserves more bound variable names);
|
file |
diff |
annotate
|
| Wed, 16 Jan 2002 23:17:44 +0100 |
wenzelm |
interface to Pattern.rewrite_term;
|
file |
diff |
annotate
|
| Wed, 16 Jan 2002 20:58:27 +0100 |
wenzelm |
export beta_eta_conversion;
|
file |
diff |
annotate
|
| Thu, 27 Dec 2001 16:46:52 +0100 |
wenzelm |
tuned tracing markup;
|
file |
diff |
annotate
|
| Sat, 24 Nov 2001 16:56:26 +0100 |
wenzelm |
gen_merge_lists;
|
file |
diff |
annotate
|
| Wed, 21 Nov 2001 00:36:51 +0100 |
wenzelm |
use tracing function for trace output;
|
file |
diff |
annotate
|
| Mon, 12 Nov 2001 10:44:55 +0100 |
berghofe |
congc now returns None if congruence rule has no effect.
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 18:01:38 +0200 |
wenzelm |
Display.pretty_thms;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 22:05:01 +0200 |
wenzelm |
tuned rewrite/simplify interface;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 20:08:11 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2001 18:29:51 +0200 |
berghofe |
Tuned comment.
|
file |
diff |
annotate
|
| Fri, 12 Oct 2001 16:57:07 +0200 |
berghofe |
- Exported goals_conv and fconv_rule
|
file |
diff |
annotate
|
| Thu, 04 Oct 2001 16:07:20 +0200 |
wenzelm |
removed obsolete comment;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2001 15:21:47 +0200 |
wenzelm |
full_rewrite_cterm_aux (see also tactic.ML);
|
file |
diff |
annotate
|
| Tue, 28 Aug 2001 14:25:26 +0200 |
nipkow |
Implemented indentation schema for conditional rewrite trace.
|
file |
diff |
annotate
|
| Thu, 23 Aug 2001 14:32:48 +0200 |
nipkow |
Traced depth of conditional rewriting
|
file |
diff |
annotate
|
| Mon, 11 Jun 2001 19:21:13 +0200 |
berghofe |
Fixed bug in function rebuild.
|
file |
diff |
annotate
|
| Thu, 10 May 2001 17:28:40 +0200 |
nipkow |
improved tracing of permutative rules.
|
file |
diff |
annotate
|