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 +
```