| Mon, 23 Jun 2008 15:26:47 +0200 |
wenzelm |
induct_tac: rule is inferred from types;
|
file |
diff |
annotate
|
| Fri, 30 May 2008 17:52:10 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 19 Oct 2005 21:52:07 +0200 |
wenzelm |
fix headers;
|
file |
diff |
annotate
|
| Fri, 18 Jan 2002 18:30:19 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2002 19:20:42 +0100 |
wenzelm |
include typedef image without path prefix!
|
file |
diff |
annotate
|
| Tue, 18 Dec 2001 18:06:10 +0100 |
paulson |
New type definition diagram
|
file |
diff |
annotate
|
| Wed, 12 Dec 2001 09:04:20 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 30 Nov 2001 17:55:13 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 29 Nov 2001 21:12:37 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Tue, 23 Oct 2001 19:13:17 +0200 |
wenzelm |
apply(simp add: three_def numerals) (* FIXME !? *);
|
file |
diff |
annotate
|
| Sun, 21 Oct 2001 19:35:40 +0200 |
wenzelm |
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
|
file |
diff |
annotate
|