| Sun, 20 Nov 2011 20:26:13 +0100 |
wenzelm |
explicit is better than implicit;
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 08:37:20 +0200 |
bulwahn |
removing old code generator setup for function types
|
file |
diff |
annotate
|
| Wed, 14 Sep 2011 10:08:52 -0400 |
hoelzl |
renamed Complete_Lattices lemmas, removed legacy names
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Sat, 10 Sep 2011 10:29:24 +0200 |
haftmann |
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 14:25:16 +0200 |
nipkow |
added new lemmas
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 13:25:17 +0200 |
haftmann |
moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
|
file |
diff |
annotate
|
| Wed, 27 Jul 2011 19:34:30 +0200 |
hoelzl |
finite vimage on arbitrary domains
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 22:25:14 +0200 |
haftmann |
more on complement
|
file |
diff |
annotate
|
| Thu, 07 Jul 2011 21:53:53 +0200 |
nipkow |
added translation to fix critical pair between abbreviations for surj and ~=
|
file |
diff |
annotate
|
| Fri, 20 May 2011 21:38:32 +0200 |
hoelzl |
add surj_vimage_empty
|
file |
diff |
annotate
|
| Tue, 05 Apr 2011 11:44:34 +0200 |
blanchet |
added "no_atp" to Cantor's paradox
|
file |
diff |
annotate
|
| Fri, 21 Jan 2011 09:44:12 +0100 |
haftmann |
moved theorem
|
file |
diff |
annotate
|
| Tue, 11 Jan 2011 14:12:37 +0100 |
haftmann |
"enriched_type" replaces less specific "type_lifting"
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 17:43:54 +0100 |
wenzelm |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 09:25:05 +0100 |
haftmann |
moved bootstrap of type_lifting to Fun
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 09:19:10 +0100 |
haftmann |
replace `type_mapper` by the more adequate `type_lifting`
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 21:09:36 +0100 |
wenzelm |
keep private things private, without comments;
|
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
|
| Thu, 18 Nov 2010 17:01:15 +0100 |
haftmann |
map_fun combinator in theory Fun
|
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
|
| Wed, 08 Sep 2010 10:45:55 +0200 |
nipkow |
put expand_(fun/set)_eq back in as synonyms, for compatibility
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 21:08:31 +0200 |
hoelzl |
Revert bij_betw changes to simp set (Problem in afp/Ordinals_and_Cardinals)
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 11:54:09 +0200 |
hoelzl |
Introduce surj_on and replace surj and bij by abbreviations.
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 10:45:51 +0200 |
hoelzl |
Permutation implies bij function
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 10:36:45 +0200 |
hoelzl |
bij <--> bij_betw
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 17:46:55 +0200 |
haftmann |
inj_comp and inj_fun
|
file |
diff |
annotate
|