| Sun, 22 May 2005 16:51:07 +0200 |
wenzelm |
Simplifier already setup in Pure;
|
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
|
| Tue, 06 Aug 2002 11:22:05 +0200 |
wenzelm |
sane interface for simprocs;
|
file |
diff |
annotate
|
| Wed, 15 May 2002 10:42:32 +0200 |
paulson |
better simplification of trivial existential equalities
|
file |
diff |
annotate
|
| Mon, 21 Jan 2002 14:47:55 +0100 |
paulson |
new simprules and classical rules
|
file |
diff |
annotate
|
| Tue, 15 Jan 2002 15:07:41 +0100 |
paulson |
new theorem
|
file |
diff |
annotate
|
| Sat, 12 Jan 2002 16:37:58 +0100 |
wenzelm |
renamed forall_elim_vars_safe to gen_all;
|
file |
diff |
annotate
|
| Fri, 11 Jan 2002 14:53:30 +0100 |
wenzelm |
replace gen_all by forall_elim_vars_safe;
|
file |
diff |
annotate
|
| Mon, 17 Dec 2001 14:27:18 +0100 |
nipkow |
mods due to changed 1-point simprocs (quantifier1).
|
file |
diff |
annotate
|
| Sat, 03 Nov 2001 18:42:38 +0100 |
wenzelm |
proper use of bind_thm(s);
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 22:15:07 +0200 |
wenzelm |
moved rulify to ObjectLogic;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 19:59:55 +0200 |
wenzelm |
eliminated atomize rules;
|
file |
diff |
annotate
|
| Thu, 31 May 2001 16:52:02 +0200 |
oheimb |
streamlined addIffs/delIffs, added warnings
|
file |
diff |
annotate
|
| Thu, 29 Mar 2001 13:59:54 +0200 |
nipkow |
generalization of 1 point rules for ALL
|
file |
diff |
annotate
|
| Fri, 10 Nov 2000 19:01:33 +0100 |
wenzelm |
FOL_basic_ss: simprocs moved to FOL_ss;
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 20:49:19 +0200 |
wenzelm |
rulify setup;
|
file |
diff |
annotate
|
| Tue, 05 Sep 2000 18:46:36 +0200 |
wenzelm |
iff declarations moved to clasimp.ML;
|
file |
diff |
annotate
|
| Tue, 29 Aug 2000 00:55:31 +0200 |
wenzelm |
cong setup now part of Simplifier;
|
file |
diff |
annotate
|
| Thu, 13 Jul 2000 12:56:42 +0200 |
paulson |
AddIffs now available for FOL, ZF
|
file |
diff |
annotate
|
| Fri, 31 Mar 2000 22:22:23 +0200 |
wenzelm |
added cong atts;
|
file |
diff |
annotate
|
| Wed, 15 Mar 2000 18:42:54 +0100 |
wenzelm |
clasimp: include Splitter;
|
file |
diff |
annotate
|
| Tue, 21 Sep 1999 19:11:07 +0200 |
nipkow |
Mod because of new solver interface.
|
file |
diff |
annotate
|
| Wed, 25 Aug 1999 20:45:19 +0200 |
wenzelm |
proper bootstrap of IFOL/FOL theories and packages;
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 16:33:47 +0100 |
wenzelm |
Theory.sign_of;
|
file |
diff |
annotate
|
| Wed, 13 Jan 1999 12:08:51 +0100 |
paulson |
congruence rules finally use == instead of = and <->
|
file |
diff |
annotate
|
| Thu, 24 Sep 1998 17:18:33 +0200 |
oheimb |
simplified CLASIMP_DATA
|
file |
diff |
annotate
|
| Fri, 18 Sep 1998 14:34:06 +0200 |
paulson |
Pruning of parameters and True assumptions
|
file |
diff |
annotate
|
| Wed, 12 Aug 1998 17:40:18 +0200 |
oheimb |
minor adaption for SML/NJ
|
file |
diff |
annotate
|
| Wed, 12 Aug 1998 16:21:18 +0200 |
oheimb |
the splitter is now defined as a functor
|
file |
diff |
annotate
|