diff -r 0b8dd4c8c79a -r 998ec26044c4 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Mar 09 21:17:21 2012 +0100
+++ b/src/HOL/Set.thy	Fri Mar 09 21:50:27 2012 +0100
@@ -97,28 +97,28 @@
 begin
 
 definition less_eq_set where
-  "less_eq_set A B = less_eq (\<lambda>x. member x A) (\<lambda>x. member x B)"
+  "A \<le> B \<longleftrightarrow> (\<lambda>x. member x A) \<le> (\<lambda>x. member x B)"
 
 definition less_set where
-  "less_set A B = less (\<lambda>x. member x A) (\<lambda>x. member x B)"
+  "A < B \<longleftrightarrow> (\<lambda>x. member x A) < (\<lambda>x. member x B)"
 
 definition inf_set where
-  "inf_set A B = Collect (inf (\<lambda>x. member x A) (\<lambda>x. member x B))"
+  "A \<sqinter> B = Collect ((\<lambda>x. member x A) \<sqinter> (\<lambda>x. member x B))"
 
 definition sup_set where
-  "sup_set A B = Collect (sup (\<lambda>x. member x A) (\<lambda>x. member x B))"
+  "A \<squnion> B = Collect ((\<lambda>x. member x A) \<squnion> (\<lambda>x. member x B))"
 
 definition bot_set where
-  "bot = Collect bot"
+  "\<bottom> = Collect \<bottom>"
 
 definition top_set where
-  "top = Collect top"
+  "\<top> = Collect \<top>"
 
 definition uminus_set where
-  "uminus A = Collect (uminus (\<lambda>x. member x A))"
+  "- A = Collect (- (\<lambda>x. member x A))"
 
 definition minus_set where
-  "minus_set A B = Collect (minus (\<lambda>x. member x A) (\<lambda>x. member x B))"
+  "A - B = Collect ((\<lambda>x. member x A) - (\<lambda>x. member x B))"
 
 instance proof
 qed (simp_all add: less_eq_set_def less_set_def inf_set_def sup_set_def
@@ -1907,3 +1907,4 @@
 *}
 
 end
+