| Thu, 30 Mar 1995 13:39:36 +0200 |
lcp |
Defined addss to perform simplification in a claset.
|
file |
diff |
annotate
|
| Wed, 08 Mar 1995 13:06:44 +0100 |
nipkow |
Enforced partial evaluation of mk_case_split_tac
|
file |
diff |
annotate
|
| Wed, 01 Feb 1995 17:17:35 +0100 |
nipkow |
The thm if(P,Q,R) now yields the two conditional rewrite rules P ==> Q and
|
file |
diff |
annotate
|
| Sun, 29 Jan 1995 14:02:17 +0100 |
nipkow |
Added some simplifications for ? x.
|
file |
diff |
annotate
|
| Wed, 07 Dec 1994 14:12:27 +0100 |
nipkow |
Added (? x. x=t & P) = P to the simpset.
|
file |
diff |
annotate
|
| Tue, 30 Aug 1994 10:04:49 +0200 |
nipkow |
New version of datatype.ML with primrec (Norbert).
|
file |
diff |
annotate
|
| Wed, 03 Aug 1994 11:00:40 +0200 |
nipkow |
renamed meta_obj_reflection meta_eq_to_obj_eq.
|
file |
diff |
annotate
|
| Tue, 02 Aug 1994 16:43:39 +0200 |
nipkow |
exposed meta_obj_reflection
|
file |
diff |
annotate
|
| Fri, 15 Jul 1994 13:53:18 +0200 |
nipkow |
added val eq_sym_conv = prover "(x=y) = (y=x)";
|
file |
diff |
annotate
|
| Tue, 19 Apr 1994 10:50:00 +0200 |
nipkow |
changed defns in hol.thy from = to ==
|
file |
diff |
annotate
|
| Sun, 27 Mar 1994 12:36:39 +0200 |
nipkow |
integrated permutative rewriting
|
file |
diff |
annotate
|
| Tue, 22 Mar 1994 08:31:58 +0100 |
nipkow |
Updated simpsets and a few proofs.
|
file |
diff |
annotate
|
| Tue, 15 Feb 1994 07:55:22 +0100 |
nipkow |
added etac FalseE to the simplifier's solver.
|
file |
diff |
annotate
|
| Thu, 03 Feb 1994 09:55:47 +0100 |
nipkow |
Introduction of various new lemmas and of case_tac.
|
file |
diff |
annotate
|
| Mon, 24 Jan 1994 15:59:02 +0100 |
nipkow |
added conj_assoc to HOL_ss
|
file |
diff |
annotate
|
| Fri, 07 Jan 1994 14:23:13 +0100 |
nipkow |
added let_weak_cong
|
file |
diff |
annotate
|
| Wed, 05 Jan 1994 19:39:05 +0100 |
nipkow |
modified solver of HOL_ss to take the new simplifier into account: the thm to
|
file |
diff |
annotate
|
| Tue, 28 Sep 1993 14:27:31 +0100 |
lcp |
This repeats a previous commit, which failed to update simpdata.ML because
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 14:29:14 +0200 |
nipkow |
defined addcongs locally in simpdata.ML
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:21:07 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|