| Mon, 19 Jul 1999 15:24:35 +0200 |
paulson |
getting rid of qed_goal
|
file |
diff |
annotate
|
| Wed, 09 Jun 1999 12:02:31 +0200 |
nipkow |
Stefan Merz's lemmas.
|
file |
diff |
annotate
|
| Wed, 15 Jul 1998 10:58:44 +0200 |
nipkow |
Minor tidying up.
|
file |
diff |
annotate
|
| Wed, 15 Jul 1998 10:15:13 +0200 |
paulson |
Removal of leading "\!\!..." from most Goal commands
|
file |
diff |
annotate
|
| Mon, 22 Jun 1998 17:26:46 +0200 |
wenzelm |
isatool fixgoal;
|
file |
diff |
annotate
|
| Tue, 24 Mar 1998 15:49:32 +0100 |
oheimb |
added finite_acyclic_wf_converse: corrected 8bit chars
|
file |
diff |
annotate
|
| Tue, 24 Mar 1998 15:46:08 +0100 |
oheimb |
added finite_acyclic_wf_converse
|
file |
diff |
annotate
|
| Sun, 22 Feb 1998 14:12:23 +0100 |
nipkow |
New induction schemas for lists (length and snoc).
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:13:18 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
| Fri, 26 Sep 1997 10:21:14 +0200 |
paulson |
Minor tidying to use Clarify_tac, etc.
|
file |
diff |
annotate
|
| Wed, 02 Jul 1997 11:59:10 +0200 |
nipkow |
Added the following lemmas tp Divides and a few others to Arith and NatDef:
|
file |
diff |
annotate
|
| Mon, 23 Jun 1997 10:42:03 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Wed, 18 Jun 1997 15:31:31 +0200 |
paulson |
Addition of not_imp (which pushes negation into implication) as a default
|
file |
diff |
annotate
|
| Fri, 13 Jun 1997 10:35:13 +0200 |
nipkow |
Tuned wf_iff_no_infinite_down_chain proof, based on Konrads ideas.
|
file |
diff |
annotate
|
| Thu, 05 Jun 1997 14:39:22 +0200 |
nipkow |
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
|
file |
diff |
annotate
|
| Thu, 22 May 1997 15:09:37 +0200 |
paulson |
Deleted rprod: lex_prod is (usually?) enough
|
file |
diff |
annotate
|
| Tue, 20 May 1997 11:40:28 +0200 |
paulson |
Relation "less_than" internalizes "<" for easy use of TFL
|
file |
diff |
annotate
|
| Thu, 15 May 1997 12:45:42 +0200 |
paulson |
New theories used by TFL
|
file |
diff |
annotate
|