| Wed, 07 Feb 2007 18:00:38 +0100 |
berghofe |
Fixed bug in mk_AbsP.
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 00:30:38 +0100 |
wenzelm |
thm/prf: separate official name vs. additional tags;
|
file |
diff |
annotate
|
| Tue, 06 Jun 2006 20:42:28 +0200 |
wenzelm |
tuned;
|
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
|
| Fri, 11 Feb 2005 18:51:00 +0100 |
berghofe |
Fully qualified refl and trans to avoid confusion with theorems
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Wed, 23 Apr 2003 00:12:14 +0200 |
berghofe |
elim_cong now eta-expands proofs on the fly if required.
|
file |
diff |
annotate
|
| Mon, 30 Sep 2002 16:27:38 +0200 |
berghofe |
- additional congruence rules for boolean operators
|
file |
diff |
annotate
|
| Sun, 21 Jul 2002 15:43:14 +0200 |
berghofe |
Rules for rewriting HOL proofs.
|
file |
diff |
annotate
|