| 2011-08-18 |
haftmann |
moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
|
file |
diff |
annotate
|
| 2011-07-27 |
hoelzl |
finite vimage on arbitrary domains
|
file |
diff |
annotate
|
| 2011-07-17 |
haftmann |
more on complement
|
file |
diff |
annotate
|
| 2011-07-07 |
nipkow |
added translation to fix critical pair between abbreviations for surj and ~=
|
file |
diff |
annotate
|
| 2011-05-20 |
hoelzl |
add surj_vimage_empty
|
file |
diff |
annotate
|
| 2011-04-05 |
blanchet |
added "no_atp" to Cantor's paradox
|
file |
diff |
annotate
|
| 2011-01-21 |
haftmann |
moved theorem
|
file |
diff |
annotate
|
| 2011-01-11 |
haftmann |
"enriched_type" replaces less specific "type_lifting"
|
file |
diff |
annotate
|
| 2010-12-17 |
wenzelm |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
file |
diff |
annotate
|
| 2010-12-06 |
haftmann |
moved bootstrap of type_lifting to Fun
|
file |
diff |
annotate
|
| 2010-12-06 |
haftmann |
replace `type_mapper` by the more adequate `type_lifting`
|
file |
diff |
annotate
|
| 2010-11-26 |
wenzelm |
keep private things private, without comments;
|
file |
diff |
annotate
|
| 2010-11-23 |
hoelzl |
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
|
file |
diff |
annotate
|
| 2010-11-22 |
hoelzl |
Replace surj by abbreviation; remove surj_on.
|
file |
diff |
annotate
|
| 2010-11-18 |
haftmann |
map_fun combinator in theory Fun
|
file |
diff |
annotate
|
| 2010-09-13 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| 2010-09-08 |
nipkow |
put expand_(fun/set)_eq back in as synonyms, for compatibility
|
file |
diff |
annotate
|
| 2010-09-07 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| 2010-09-02 |
hoelzl |
Revert bij_betw changes to simp set (Problem in afp/Ordinals_and_Cardinals)
|
file |
diff |
annotate
|
| 2010-09-02 |
hoelzl |
Introduce surj_on and replace surj and bij by abbreviations.
|
file |
diff |
annotate
|
| 2010-09-02 |
hoelzl |
Permutation implies bij function
|
file |
diff |
annotate
|
| 2010-09-02 |
hoelzl |
bij <--> bij_betw
|
file |
diff |
annotate
|
| 2010-08-20 |
haftmann |
inj_comp and inj_fun
|
file |
diff |
annotate
|
| 2010-07-12 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| 2010-07-09 |
haftmann |
nicer xsymbol syntax for fcomp and scomp
|
file |
diff |
annotate
|
| 2010-04-16 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
| 2010-03-05 |
hoelzl |
generalized inj_uminus; added strict_mono_imp_inj_on
|
file |
diff |
annotate
|
| 2010-03-04 |
hoelzl |
Rewrite rules for images of minus of intervals
|
file |
diff |
annotate
|
| 2010-03-01 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| 2010-02-11 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
| 2009-12-30 |
krauss |
killed a few warnings
|
file |
diff |
annotate
|
| 2009-12-21 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2009-12-21 |
haftmann |
moved lemmas o_eq_dest, o_eq_elim here
|
file |
diff |
annotate
|
| 2009-12-19 |
huffman |
add lemma swap_triple
|
file |
diff |
annotate
|
| 2009-12-16 |
huffman |
declare swap_self [simp], add lemma comp_swap
|
file |
diff |
annotate
|
| 2009-10-29 |
haftmann |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
file |
diff |
annotate
|
| 2009-10-22 |
nipkow |
inv_onto -> inv_into
|
file |
diff |
annotate
|
| 2009-10-20 |
paulson |
Some new lemmas concerning sets
|
file |
diff |
annotate
|
| 2009-10-19 |
berghofe |
Renamed inv to the_inv and turned it into an abbreviation (based on the_inv_onto).
|
file |
diff |
annotate
|
| 2009-10-18 |
nipkow |
Inv -> inv_onto, inv abbr. inv_onto UNIV.
|
file |
diff |
annotate
|
| 2009-10-17 |
nipkow |
added the_inv_onto
|
file |
diff |
annotate
|
| 2009-09-29 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| 2009-09-10 |
haftmann |
early bootstrap of generic transfer procedure
|
file |
diff |
annotate
|
| 2009-08-10 |
nipkow |
new lemma bij_comp
|
file |
diff |
annotate
|
| 2009-07-22 |
haftmann |
moved complete_lattice &c. into separate theory
|
file |
diff |
annotate
|
| 2009-07-06 |
haftmann |
moved Inductive.myinv to Fun.inv; tuned
|
file |
diff |
annotate
|
| 2009-06-23 |
haftmann |
uniformly capitialized names for subdirectories
|
file |
diff |
annotate
|
| 2009-06-10 |
haftmann |
separate directory for datatype package
|
file |
diff |
annotate
|
| 2009-06-04 |
nipkow |
A few finite lemmas
|
file |
diff |
annotate
|
| 2009-05-19 |
haftmann |
pretty printing of functional combinators for evaluation code
|
file |
diff |
annotate
|
| 2009-05-09 |
nipkow |
lemmas by Andreas Lochbihler
|
file |
diff |
annotate
|
| 2009-03-05 |
haftmann |
dropped Id
|
file |
diff |
annotate
|
| 2008-10-31 |
berghofe |
Replaced arbitrary by undefined.
|
file |
diff |
annotate
|
| 2008-10-10 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| 2008-06-23 |
wenzelm |
Logic.all/mk_equals/mk_implies;
|
file |
diff |
annotate
|
| 2008-06-13 |
nipkow |
hide -> hide (open)
|
file |
diff |
annotate
|
| 2008-06-12 |
nipkow |
Hid swap
|
file |
diff |
annotate
|
| 2008-06-10 |
wenzelm |
tuned proofs -- case_tac *is* available here;
|
file |
diff |
annotate
|
| 2008-06-10 |
haftmann |
removed some dubious code lemmas
|
file |
diff |
annotate
|
| 2008-04-09 |
haftmann |
removed syntax from monad combinators; renamed mbind to scomp
|
file |
diff |
annotate
|