| Wed, 28 Jun 2000 10:46:25 +0200 |
paulson |
updated and tidied
|
file |
diff |
annotate
|
| Thu, 22 Jun 2000 23:04:34 +0200 |
wenzelm |
bind_thm(s);
|
file |
diff |
annotate
|
| Fri, 16 Jun 2000 13:16:07 +0200 |
paulson |
renamed psubset_card -> psubset_card_mono
|
file |
diff |
annotate
|
| Thu, 13 Apr 2000 15:01:50 +0200 |
nipkow |
Times -> <*>
|
file |
diff |
annotate
|
| Wed, 22 Mar 2000 13:23:57 +0100 |
paulson |
made a proof more robust (did not like Suc_less_eq)
|
file |
diff |
annotate
|
| Fri, 18 Feb 2000 15:34:22 +0100 |
paulson |
expandshort
|
file |
diff |
annotate
|
| Fri, 28 Jan 2000 14:09:23 +0100 |
oheimb |
added full_nat_induct
|
file |
diff |
annotate
|
| 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
|