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
|
Mon, 18 Oct 1999 18:38:21 +0200 |
wenzelm |
update by Stephan Merz;
|
file |
diff |
annotate
|
Mon, 08 Feb 1999 13:02:56 +0100 |
wenzelm |
updated (Stephan Merz);
|
file |
diff |
annotate
|
Fri, 23 Oct 1998 20:35:19 +0200 |
oheimb |
corrected auto_tac (applications of unsafe wrappers)
|
file |
diff |
annotate
|
Mon, 21 Sep 1998 23:17:28 +0200 |
oheimb |
improved addbefore and addSbefore
|
file |
diff |
annotate
|
Fri, 24 Jul 1998 08:10:04 +0200 |
nipkow |
induct_tac -> exhaust_tac in 2 places.
|
file |
diff |
annotate
|
Mon, 22 Jun 1998 17:26:46 +0200 |
wenzelm |
isatool fixgoal;
|
file |
diff |
annotate
|
Wed, 24 Dec 1997 10:02:30 +0100 |
paulson |
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
|
file |
diff |
annotate
|
Mon, 03 Nov 1997 12:13:18 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
Wed, 08 Oct 1997 11:50:33 +0200 |
wenzelm |
A formalization of TLA in HOL -- by Stephan Merz;
|
file |
diff |
annotate
|