Wed, 31 Jan 2001 10:13:22 +0100 |
oheimb |
shortened proof of some1_equality
|
file |
diff |
annotate
|
Sat, 23 Dec 2000 22:49:39 +0100 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
Fri, 10 Nov 2000 19:03:06 +0100 |
wenzelm |
axclass power moved to Nat.thy;
|
file |
diff |
annotate
|
Tue, 17 Oct 2000 10:21:12 +0200 |
paulson |
renaming of contrapos rules
|
file |
diff |
annotate
|
Mon, 09 Oct 2000 14:10:55 +0200 |
nipkow |
ex_someI -> someI_ex
|
file |
diff |
annotate
|
Mon, 09 Oct 2000 09:33:45 +0200 |
nipkow |
@ -> SOME
|
file |
diff |
annotate
|
Fri, 22 Sep 2000 17:25:09 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
Fri, 15 Sep 2000 20:22:00 +0200 |
wenzelm |
fixed someI2_ex;
|
file |
diff |
annotate
|
Fri, 15 Sep 2000 15:30:50 +0200 |
paulson |
the final renaming: selectI -> someI
|
file |
diff |
annotate
|
Fri, 15 Sep 2000 12:39:57 +0200 |
paulson |
renamed (most of...) the select rules
|
file |
diff |
annotate
|
Tue, 05 Sep 2000 21:06:01 +0200 |
wenzelm |
improved meson setup;
|
file |
diff |
annotate
|
Wed, 30 Aug 2000 10:21:19 +0200 |
nipkow |
Fixed rulify.
|
file |
diff |
annotate
|
Fri, 04 Aug 2000 22:56:11 +0200 |
wenzelm |
removed stac (now exported by HypsubstFun);
|
file |
diff |
annotate
|
Fri, 21 Jul 2000 18:11:54 +0200 |
nipkow |
added ex_someI
|
file |
diff |
annotate
|
Wed, 28 Jun 2000 10:39:02 +0200 |
paulson |
rev_notE now makes strong elim rules;
|
file |
diff |
annotate
|
Tue, 13 Jun 2000 18:33:34 +0200 |
wenzelm |
qed_spec_mp: strip_shyps_warning;
|
file |
diff |
annotate
|
Wed, 24 May 2000 18:51:28 +0200 |
paulson |
some lemmas about plus_ac0
|
file |
diff |
annotate
|
Mon, 20 Mar 2000 18:25:35 +0100 |
paulson |
tidied
|
file |
diff |
annotate
|
Tue, 22 Feb 2000 21:39:38 +0100 |
wenzelm |
removed case_split thm binding;
|
file |
diff |
annotate
|
Tue, 19 Oct 1999 16:23:46 +0200 |
wenzelm |
qed_spec_mp is a mess;
|
file |
diff |
annotate
|
Mon, 11 Oct 1999 20:43:38 +0200 |
wenzelm |
bind_thm "ccontr";
|
file |
diff |
annotate
|
Wed, 29 Sep 1999 16:45:23 +0200 |
wenzelm |
bind_thm ("case_split", case_split_thm);
|
file |
diff |
annotate
|
Tue, 28 Sep 1999 13:37:54 +0200 |
paulson |
more tidying
|
file |
diff |
annotate
|
Tue, 21 Sep 1999 17:28:02 +0200 |
wenzelm |
removed "case" thm;
|
file |
diff |
annotate
|
Thu, 09 Sep 1999 14:30:08 +0200 |
oheimb |
minor change to smp_tac
|
file |
diff |
annotate
|
Mon, 06 Sep 1999 18:17:48 +0200 |
oheimb |
added smp_tac
|
file |
diff |
annotate
|
Wed, 01 Sep 1999 21:25:17 +0200 |
wenzelm |
bind_thm "case";
|
file |
diff |
annotate
|
Wed, 25 Aug 1999 20:49:02 +0200 |
wenzelm |
proper bootstrap of HOL theory and packages;
|
file |
diff |
annotate
|