equal
deleted
inserted
replaced
50 defs (overloaded) |
50 defs (overloaded) |
51 func_one: "1::(('a::type) => ('b::one)) == %x. 1" |
51 func_one: "1::(('a::type) => ('b::one)) == %x. 1" |
52 set_one: "1::('a::one)set == {1}" |
52 set_one: "1::('a::one)set == {1}" |
53 |
53 |
54 definition |
54 definition |
55 elt_set_plus :: "'a::plus => 'a set => 'a set" (infixl "+o" 70) |
55 elt_set_plus :: "'a::plus => 'a set => 'a set" (infixl "+o" 70) where |
56 "a +o B = {c. EX b:B. c = a + b}" |
56 "a +o B = {c. EX b:B. c = a + b}" |
57 |
57 |
58 elt_set_times :: "'a::times => 'a set => 'a set" (infixl "*o" 80) |
58 definition |
|
59 elt_set_times :: "'a::times => 'a set => 'a set" (infixl "*o" 80) where |
59 "a *o B = {c. EX b:B. c = a * b}" |
60 "a *o B = {c. EX b:B. c = a * b}" |
60 |
61 |
61 abbreviation (input) |
62 abbreviation (input) |
62 elt_set_eq :: "'a => 'a set => bool" (infix "=o" 50) |
63 elt_set_eq :: "'a => 'a set => bool" (infix "=o" 50) where |
63 "x =o A == x : A" |
64 "x =o A == x : A" |
64 |
65 |
65 instance "fun" :: (type,semigroup_add)semigroup_add |
66 instance "fun" :: (type,semigroup_add)semigroup_add |
66 by default (auto simp add: func_plus add_assoc) |
67 by default (auto simp add: func_plus add_assoc) |
67 |
68 |