src/HOL/Predicate_Compile.thy
 changeset 67613 ce654b0e6d69 parent 63432 ba7901e94e7b child 69593 3dda49e08b9d
```     1.1 --- a/src/HOL/Predicate_Compile.thy	Tue Feb 13 14:24:50 2018 +0100
1.2 +++ b/src/HOL/Predicate_Compile.thy	Thu Feb 15 12:11:00 2018 +0100
1.3 @@ -32,10 +32,10 @@
1.4  \<close>
1.5
1.6  definition contains :: "'a set => 'a => bool"
1.7 -where "contains A x \<longleftrightarrow> x : A"
1.8 +where "contains A x \<longleftrightarrow> x \<in> A"
1.9
1.10  definition contains_pred :: "'a set => 'a => unit Predicate.pred"
1.11 -where "contains_pred A x = (if x : A then Predicate.single () else bot)"
1.12 +where "contains_pred A x = (if x \<in> A then Predicate.single () else bot)"
1.13
1.14  lemma pred_of_setE:
1.15    assumes "Predicate.eval (pred_of_set A) x"
1.16 @@ -52,7 +52,7 @@
1.17  by(simp add: contains_def)
1.18
1.19  lemma containsE: assumes "contains A x"
1.20 -  obtains A' x' where "A = A'" "x = x'" "x : A"
1.21 +  obtains A' x' where "A = A'" "x = x'" "x \<in> A"
1.22  using assms by(simp add: contains_def)
1.23
1.24  lemma contains_predI: "contains A x ==> Predicate.eval (contains_pred A x) ()"
```