| Wed, 30 Aug 2000 16:29:21 +0200 |
nipkow |
introduced induct_thm_tac
|
file |
diff |
annotate
|
| Fri, 23 Jun 2000 10:34:31 +0200 |
paulson |
genPrefix_trans_O: generalizes genPrefix_trans
|
file |
diff |
annotate
|
| Mon, 13 Mar 2000 16:23:34 +0100 |
wenzelm |
case_tac now subsumes both boolean and datatype cases;
|
file |
diff |
annotate
|
| Mon, 13 Mar 2000 12:51:10 +0100 |
nipkow |
exhaust_tac -> cases_tac
|
file |
diff |
annotate
|
| Wed, 09 Feb 2000 11:45:10 +0100 |
paulson |
updated the Client example
|
file |
diff |
annotate
|
| Fri, 14 Jan 2000 12:17:53 +0100 |
paulson |
still working; a bit of polishing
|
file |
diff |
annotate
|
| Fri, 17 Dec 1999 10:30:48 +0100 |
paulson |
now workign as far as System_Alloc_Progress
|
file |
diff |
annotate
|
| Wed, 13 Oct 1999 12:03:22 +0200 |
paulson |
new theorem set_mono
|
file |
diff |
annotate
|
| Tue, 07 Sep 1999 10:40:58 +0200 |
wenzelm |
isatool expandshort;
|
file |
diff |
annotate
|
| Wed, 21 Jul 1999 15:17:30 +0200 |
paulson |
tweaked proof after removal of diff_is_0_eq RS iffD2
|
file |
diff |
annotate
|
| Sun, 13 Jun 1999 13:54:34 +0200 |
paulson |
renamed pfix_[lg}e
|
file |
diff |
annotate
|
| Thu, 10 Jun 1999 10:24:32 +0200 |
paulson |
Generalized prefix theory, replacing the reference to directory Lex.
|
file |
diff |
annotate
|