| Tue, 21 Sep 1999 17:29:46 +0200 |
wenzelm |
Thm.no_prems;
|
file |
diff |
annotate
|
| Fri, 14 Aug 1998 12:02:35 +0200 |
paulson |
Uses Goal instead of "goal...thy" to avoid theory problems
|
file |
diff |
annotate
|
| Fri, 27 Feb 1998 11:08:20 +0100 |
paulson |
"choice" moved to Set.ML
|
file |
diff |
annotate
|
| Fri, 19 Dec 1997 10:27:23 +0100 |
wenzelm |
adapted to new sort function;
|
file |
diff |
annotate
|
| Fri, 21 Nov 1997 15:29:56 +0100 |
wenzelm |
changed Pure/Sequence interface -- isatool fixseq;
|
file |
diff |
annotate
|
| Wed, 05 Nov 1997 13:23:46 +0100 |
paulson |
Ran expandshort, especially to introduce Safe_tac
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:13:18 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
| Fri, 10 Oct 1997 19:02:28 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Tue, 22 Jul 1997 11:12:55 +0200 |
paulson |
Removal of the tactical STATE
|
file |
diff |
annotate
|
| Wed, 05 Mar 1997 09:59:24 +0100 |
paulson |
Renamed constant "not" to "Not"
|
file |
diff |
annotate
|
| Thu, 26 Sep 1996 12:47:47 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Fri, 21 Jun 1996 12:18:50 +0200 |
berghofe |
Classical tactics now use default claset.
|
file |
diff |
annotate
|
| Fri, 24 May 1996 11:42:04 +0200 |
paulson |
Augmented comment about conversion to clauses
|
file |
diff |
annotate
|
| Thu, 21 Mar 1996 11:11:47 +0100 |
paulson |
Now labels the Horn and goal clauses to make the proof
|
file |
diff |
annotate
|
| Fri, 15 Mar 1996 18:42:36 +0100 |
paulson |
New safe_meson_tac uses iterative deepening
|
file |
diff |
annotate
|
| Fri, 16 Feb 1996 18:00:47 +0100 |
paulson |
Elimination of fully-functorial style.
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 15:24:36 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Wed, 22 Mar 1995 12:42:34 +0100 |
clasohm |
converted ex with curried function application
|
file |
diff |
annotate
|