| Thu, 07 Apr 2011 13:01:27 +0200 |
haftmann |
dropped unused lemmas; proper Isar proof
|
file |
diff |
annotate
|
| Sun, 03 Apr 2011 11:40:32 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Sat, 02 Apr 2011 18:07:29 +0200 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
| Thu, 17 Mar 2011 09:58:13 +0100 |
nipkow |
tuned lemma
|
file |
diff |
annotate
|
| Wed, 16 Mar 2011 19:50:56 +0100 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Fri, 21 Jan 2011 09:44:12 +0100 |
haftmann |
moved theorem
|
file |
diff |
annotate
|
| Fri, 21 Jan 2011 09:41:59 +0100 |
haftmann |
restructured theory;
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 20:38:58 +0100 |
wenzelm |
recoded latin1 as utf8;
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
adding code equation for finiteness of finite types
|
file |
diff |
annotate
|
| Sun, 28 Nov 2010 15:20:51 +0100 |
nipkow |
gave more standard finite set rules simp and intro attribute
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 18:06:48 +0100 |
nipkow |
new lemma
|
file |
diff |
annotate
|
| Tue, 23 Nov 2010 14:14:17 +0100 |
hoelzl |
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 10:34:33 +0100 |
hoelzl |
Replace surj by abbreviation; remove surj_on.
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 08:29:32 +0100 |
nipkow |
removed assumption
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Fri, 13 Aug 2010 10:51:23 +0200 |
haftmann |
import swap prevents strange failure of SML code generator for datatypes
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 11:39:27 +0200 |
haftmann |
avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 16:54:44 +0200 |
haftmann |
"prod" and "sum" replace "*" and "+" respectively
|
file |
diff |
annotate
|
| Fri, 18 Jun 2010 22:40:58 +0200 |
nipkow |
added pigeonhole lemmas
|
file |
diff |
annotate
|
| Tue, 04 May 2010 10:02:43 +0200 |
haftmann |
avoid if on rhs of default simp rules
|
file |
diff |
annotate
|
| Tue, 04 May 2010 08:55:43 +0200 |
haftmann |
locale predicates of classes carry a mandatory "class" prefix
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
| Wed, 07 Apr 2010 11:05:11 +0200 |
Christian Urban |
simplified induction case in finite_psubset_induct; tuned the proof that uses this induction principle
|
file |
diff |
annotate
|
| Tue, 30 Mar 2010 15:46:50 -0700 |
huffman |
simplify fold_graph proofs
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 13:59:20 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 13:56:32 +0100 |
haftmann |
added locales folding_one_(idem); various streamlining and tuning
|
file |
diff |
annotate
|