| Wed, 07 Sep 2005 20:22:39 +0200 |
wenzelm |
converted to Isar theory format;
|
file |
diff |
annotate
|
| Tue, 17 Oct 2000 10:21:12 +0200 |
paulson |
renaming of contrapos rules
|
file |
diff |
annotate
|
| Thu, 03 Aug 2000 19:29:03 +0200 |
wenzelm |
tuned version by Stephan Merz (unbatchified etc.);
|
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
|
| 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 13:19:38 +0200 |
berghofe |
Adapted to new datatype package.
|
file |
diff |
annotate
|
| Fri, 24 Apr 1998 16:18:39 +0200 |
oheimb |
improved split_all_tac significantly
|
file |
diff |
annotate
|
| Thu, 12 Mar 1998 13:17:13 +0100 |
oheimb |
renamed not1_or to disj_not1, not2_or to disj_not2
|
file |
diff |
annotate
|
| Tue, 10 Mar 1998 18:32:08 +0100 |
oheimb |
added not1_or and if_eq_cancel to simpset()
|
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
|