| Tue, 28 Feb 1995 02:00:28 +0100 |
lcp |
Proved less_eq_Suc_add and add_left_cancel (cf left_plus_cancel on
|
file |
diff |
annotate
|
| Wed, 14 Dec 1994 11:17:18 +0100 |
clasohm |
added bind_thm for theorems made by "standard ..."
Isabelle94-2
|
file |
diff |
annotate
|
| Fri, 25 Nov 1994 09:12:16 +0100 |
clasohm |
replaced prove_goal by qed_goal
|
file |
diff |
annotate
|
| Mon, 21 Nov 1994 17:50:34 +0100 |
clasohm |
replaced 'val ... = result()' by 'qed "..."'
|
file |
diff |
annotate
|
| Wed, 29 Jun 1994 12:04:04 +0200 |
clasohm |
added parentheses made necessary by change of constrain's precedence
|
file |
diff |
annotate
|
| Fri, 17 Jun 1994 18:34:12 +0200 |
lcp |
HOL/Arith/add_left_commute: tidied
|
file |
diff |
annotate
|
| Wed, 25 May 1994 13:03:19 +0200 |
lcp |
HOL/Arith: definition of diff now uses pred, not nat_rec
|
file |
diff |
annotate
|
| Thu, 21 Apr 1994 11:13:22 +0200 |
lcp |
HOL/arith.ML/plus_leD1: tidied
|
file |
diff |
annotate
|
| Sun, 27 Mar 1994 12:36:39 +0200 |
nipkow |
integrated permutative rewriting
|
file |
diff |
annotate
|
| Tue, 22 Mar 1994 08:25:30 +0100 |
nipkow |
used ordered rewriting to simplify some proofs
|
file |
diff |
annotate
|
| Wed, 16 Feb 1994 15:13:53 +0100 |
nipkow |
added more lemmas (also to nat_ss)
|
file |
diff |
annotate
|
| Thu, 03 Feb 1994 09:55:47 +0100 |
nipkow |
Introduction of various new lemmas and of case_tac.
|
file |
diff |
annotate
|
| Wed, 05 Jan 1994 19:37:07 +0100 |
nipkow |
added new rewrite rules to arith_ss
|
file |
diff |
annotate
|
| Tue, 30 Nov 1993 17:44:04 +0100 |
nipkow |
added pred: nat=>nat
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:21:07 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|