Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/SetsAndFunctions.thy
changeset 21404 eb85850d3eb7
parent 20523 36a59e5d0039
child 23477 f4b83f03cac9 
--- a/src/HOL/Library/SetsAndFunctions.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Library/SetsAndFunctions.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -52,14 +52,15 @@
   set_one: "1::('a::one)set == {1}"
 
 definition
-  elt_set_plus :: "'a::plus => 'a set => 'a set"    (infixl "+o" 70)
+  elt_set_plus :: "'a::plus => 'a set => 'a set"  (infixl "+o" 70) where
   "a +o B = {c. EX b:B. c = a + b}"
 
-  elt_set_times :: "'a::times => 'a set => 'a set"  (infixl "*o" 80)
+definition
+  elt_set_times :: "'a::times => 'a set => 'a set"  (infixl "*o" 80) where
   "a *o B = {c. EX b:B. c = a * b}"
 
 abbreviation (input)
-  elt_set_eq :: "'a => 'a set => bool"      (infix "=o" 50)
+  elt_set_eq :: "'a => 'a set => bool"  (infix "=o" 50) where
   "x =o A == x : A"
 
 instance "fun" :: (type,semigroup_add)semigroup_add
isabelle