| Sat, 30 May 2009 11:57:36 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 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.
|
file |
diff |
annotate
|
| Mon, 16 Mar 2009 23:36:55 +0100 |
wenzelm |
provide Simplifier.norm_hhf(_protect) as regular simplifier operation;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 12:15:58 +0100 |
wenzelm |
added dest_ss;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 11:45:56 +0100 |
wenzelm |
renamed rep_ss to MetaSimplifier.internal_ss;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2009 22:32:27 +0100 |
wenzelm |
replaced archaic use of rep_ss by Simplifier.mksimps;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 15:30:10 +0100 |
wenzelm |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 22:44:29 +0200 |
wenzelm |
Drule.norm_hhf_eqs;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 16:52:46 +0200 |
wenzelm |
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
|
file |
diff |
annotate
|
| Mon, 14 Jul 2008 19:20:57 +0200 |
haftmann |
dropped junk
|
file |
diff |
annotate
|
| Mon, 14 Jul 2008 11:04:47 +0200 |
haftmann |
added further simple interfaces
|
file |
diff |
annotate
|
| Sat, 21 Jun 2008 16:18:49 +0200 |
wenzelm |
activate_context: strict the_context, no fallback on theory context;
|
file |
diff |
annotate
|
| Thu, 29 May 2008 23:46:45 +0200 |
wenzelm |
legacy_feature: no proof context in simpset;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:35 +0200 |
wenzelm |
rep_cterm/rep_thm: no longer dereference theory_ref;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 14:41:09 +0100 |
wenzelm |
eliminated theory ProtoPure;
|
file |
diff |
annotate
|
| Tue, 27 Nov 2007 15:47:40 +0100 |
berghofe |
check_conv now only performs beta-eta-normalization when equations
|
file |
diff |
annotate
|
| Fri, 26 Oct 2007 17:55:33 +0200 |
wenzelm |
asm_rewrite_goal_tac: avoiding PRIMITIVE lets informative exceptions (from simprocs) get through;
|
file |
diff |
annotate
|
| 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
|