src/HOL/Set.thy
changeset 46853 998ec26044c4
parent 46504 cd4832aa2229
child 46882 6242b4bc05bc
     1.1 --- a/src/HOL/Set.thy	Fri Mar 09 21:17:21 2012 +0100
     1.2 +++ b/src/HOL/Set.thy	Fri Mar 09 21:50:27 2012 +0100
     1.3 @@ -97,28 +97,28 @@
     1.4  begin
     1.5  
     1.6  definition less_eq_set where
     1.7 -  "less_eq_set A B = less_eq (\<lambda>x. member x A) (\<lambda>x. member x B)"
     1.8 +  "A \<le> B \<longleftrightarrow> (\<lambda>x. member x A) \<le> (\<lambda>x. member x B)"
     1.9  
    1.10  definition less_set where
    1.11 -  "less_set A B = less (\<lambda>x. member x A) (\<lambda>x. member x B)"
    1.12 +  "A < B \<longleftrightarrow> (\<lambda>x. member x A) < (\<lambda>x. member x B)"
    1.13  
    1.14  definition inf_set where
    1.15 -  "inf_set A B = Collect (inf (\<lambda>x. member x A) (\<lambda>x. member x B))"
    1.16 +  "A \<sqinter> B = Collect ((\<lambda>x. member x A) \<sqinter> (\<lambda>x. member x B))"
    1.17  
    1.18  definition sup_set where
    1.19 -  "sup_set A B = Collect (sup (\<lambda>x. member x A) (\<lambda>x. member x B))"
    1.20 +  "A \<squnion> B = Collect ((\<lambda>x. member x A) \<squnion> (\<lambda>x. member x B))"
    1.21  
    1.22  definition bot_set where
    1.23 -  "bot = Collect bot"
    1.24 +  "\<bottom> = Collect \<bottom>"
    1.25  
    1.26  definition top_set where
    1.27 -  "top = Collect top"
    1.28 +  "\<top> = Collect \<top>"
    1.29  
    1.30  definition uminus_set where
    1.31 -  "uminus A = Collect (uminus (\<lambda>x. member x A))"
    1.32 +  "- A = Collect (- (\<lambda>x. member x A))"
    1.33  
    1.34  definition minus_set where
    1.35 -  "minus_set A B = Collect (minus (\<lambda>x. member x A) (\<lambda>x. member x B))"
    1.36 +  "A - B = Collect ((\<lambda>x. member x A) - (\<lambda>x. member x B))"
    1.37  
    1.38  instance proof
    1.39  qed (simp_all add: less_eq_set_def less_set_def inf_set_def sup_set_def
    1.40 @@ -1907,3 +1907,4 @@
    1.41  *}
    1.42  
    1.43  end
    1.44 +