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) ()"