diff -r 0c18df79b1c8 -r a642599ffdea src/ZF/Constructible/Relative.thy
--- a/src/ZF/Constructible/Relative.thy	Tue Sep 27 17:03:23 2022 +0100
+++ b/src/ZF/Constructible/Relative.thy	Tue Sep 27 17:46:52 2022 +0100
@@ -11,120 +11,120 @@
 subsection\<open>Relativized versions of standard set-theoretic concepts\<close>
 
 definition
-  empty :: "[i=>o,i] => o" where
+  empty :: "[i\<Rightarrow>o,i] \<Rightarrow> o" where
     "empty(M,z) \<equiv> \<forall>x[M]. x \<notin> z"
 
 definition
-  subset :: "[i=>o,i,i] => o" where
+  subset :: "[i\<Rightarrow>o,i,i] \<Rightarrow> o" where
     "subset(M,A,B) \<equiv> \<forall>x[M]. x\<in>A \<longrightarrow> x \<in> B"
 
 definition
-  upair :: "[i=>o,i,i,i] => o" where
+  upair :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
     "upair(M,a,b,z) \<equiv> a \<in> z \<and> b \<in> z \<and> (\<forall>x[M]. x\<in>z \<longrightarrow> x = a \<or> x = b)"
 
 definition
-  pair :: "[i=>o,i,i,i] => o" where
+  pair :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
     "pair(M,a,b,z) \<equiv> \<exists>x[M]. upair(M,a,a,x) \<and>
                      (\<exists>y[M]. upair(M,a,b,y) \<and> upair(M,x,y,z))"
 
 
 definition
-  union :: "[i=>o,i,i,i] => o" where
+  union :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
     "union(M,a,b,z) \<equiv> \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> a \<or> x \<in> b"
 
 definition
-  is_cons :: "[i=>o,i,i,i] => o" where
+  is_cons :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
     "is_cons(M,a,b,z) \<equiv> \<exists>x[M]. upair(M,a,a,x) \<and> union(M,x,b,z)"
 
 definition
-  successor :: "[i=>o,i,i] => o" where
+  successor :: "[i\<Rightarrow>o,i,i] \<Rightarrow> o" where
     "successor(M,a,z) \<equiv> is_cons(M,a,a,z)"
 
 definition
-  number1 :: "[i=>o,i] => o" where
+  number1 :: "[i\<Rightarrow>o,i] \<Rightarrow> o" where
     "number1(M,a) \<equiv> \<exists>x[M]. empty(M,x) \<and> successor(M,x,a)"
 
 definition
-  number2 :: "[i=>o,i] => o" where
+  number2 :: "[i\<Rightarrow>o,i] \<Rightarrow> o" where
     "number2(M,a) \<equiv> \<exists>x[M]. number1(M,x) \<and> successor(M,x,a)"
 
 definition
-  number3 :: "[i=>o,i] => o" where
+  number3 :: "[i\<Rightarrow>o,i] \<Rightarrow> o" where
     "number3(M,a) \<equiv> \<exists>x[M]. number2(M,x) \<and> successor(M,x,a)"
 
 definition
-  powerset :: "[i=>o,i,i] => o" where
+  powerset :: "[i\<Rightarrow>o,i,i] \<Rightarrow> o" where
     "powerset(M,A,z) \<equiv> \<forall>x[M]. x \<in> z \<longleftrightarrow> subset(M,x,A)"
 
 definition
-  is_Collect :: "[i=>o,i,i=>o,i] => o" where
+  is_Collect :: "[i\<Rightarrow>o,i,i\<Rightarrow>o,i] \<Rightarrow> o" where
     "is_Collect(M,A,P,z) \<equiv> \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> A \<and> P(x)"
 
 definition
-  is_Replace :: "[i=>o,i,[i,i]=>o,i] => o" where
+  is_Replace :: "[i\<Rightarrow>o,i,[i,i]\<Rightarrow>o,i] \<Rightarrow> o" where
     "is_Replace(M,A,P,z) \<equiv> \<forall>u[M]. u \<in> z \<longleftrightarrow> (\<exists>x[M]. x\<in>A \<and> P(x,u))"
 
 definition
-  inter :: "[i=>o,i,i,i] => o" where
+  inter :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
     "inter(M,a,b,z) \<equiv> \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> a \<and> x \<in> b"
 
 definition
-  setdiff :: "[i=>o,i,i,i] => o" where
+  setdiff :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
     "setdiff(M,a,b,z) \<equiv> \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> a \<and> x \<notin> b"
 
 definition
-  big_union :: "[i=>o,i,i] => o" where
+  big_union :: "[i\<Rightarrow>o,i,i] \<Rightarrow> o" where
     "big_union(M,A,z) \<equiv> \<forall>x[M]. x \<in> z \<longleftrightarrow> (\<exists>y[M]. y\<in>A \<and> x \<in> y)"
 
 definition
-  big_inter :: "[i=>o,i,i] => o" where
+  big_inter :: "[i\<Rightarrow>o,i,i] \<Rightarrow> o" where
     "big_inter(M,A,z) \<equiv>
              (A=0 \<longrightarrow> z=0) \<and>
              (A\<noteq>0 \<longrightarrow> (\<forall>x[M]. x \<in> z \<longleftrightarrow> (\<forall>y[M]. y\<in>A \<longrightarrow> x \<in> y)))"
 
 definition
-  cartprod :: "[i=>o,i,i,i] => o" where
+  cartprod :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
     "cartprod(M,A,B,z) \<equiv>
         \<forall>u[M]. u \<in> z \<longleftrightarrow> (\<exists>x[M]. x\<in>A \<and> (\<exists>y[M]. y\<in>B \<and> pair(M,x,y,u)))"
 
 definition
-  is_sum :: "[i=>o,i,i,i] => o" where
+  is_sum :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
     "is_sum(M,A,B,Z) \<equiv>
        \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M].
        number1(M,n1) \<and> cartprod(M,n1,A,A0) \<and> upair(M,n1,n1,s1) \<and>
        cartprod(M,s1,B,B1) \<and> union(M,A0,B1,Z)"
 
 definition
-  is_Inl :: "[i=>o,i,i] => o" where
+  is_Inl :: "[i\<Rightarrow>o,i,i] \<Rightarrow> o" where
     "is_Inl(M,a,z) \<equiv> \<exists>zero[M]. empty(M,zero) \<and> pair(M,zero,a,z)"
 
 definition
-  is_Inr :: "[i=>o,i,i] => o" where
+  is_Inr :: "[i\<Rightarrow>o,i,i] \<Rightarrow> o" where
     "is_Inr(M,a,z) \<equiv> \<exists>n1[M]. number1(M,n1) \<and> pair(M,n1,a,z)"
 
 definition
-  is_converse :: "[i=>o,i,i] => o" where
+  is_converse :: "[i\<Rightarrow>o,i,i] \<Rightarrow> o" where
     "is_converse(M,r,z) \<equiv>
         \<forall>x[M]. x \<in> z \<longleftrightarrow>
              (\<exists>w[M]. w\<in>r \<and> (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) \<and> pair(M,v,u,x)))"
 
 definition
-  pre_image :: "[i=>o,i,i,i] => o" where
+  pre_image :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
     "pre_image(M,r,A,z) \<equiv>
         \<forall>x[M]. x \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r \<and> (\<exists>y[M]. y\<in>A \<and> pair(M,x,y,w)))"
 
 definition
-  is_domain :: "[i=>o,i,i] => o" where
+  is_domain :: "[i\<Rightarrow>o,i,i] \<Rightarrow> o" where
     "is_domain(M,r,z) \<equiv>
         \<forall>x[M]. x \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r \<and> (\<exists>y[M]. pair(M,x,y,w)))"
 
 definition
-  image :: "[i=>o,i,i,i] => o" where
+  image :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
     "image(M,r,A,z) \<equiv>
         \<forall>y[M]. y \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r \<and> (\<exists>x[M]. x\<in>A \<and> pair(M,x,y,w)))"
 
 definition
-  is_range :: "[i=>o,i,i] => o" where
+  is_range :: "[i\<Rightarrow>o,i,i] \<Rightarrow> o" where
     \<comment> \<open>the cleaner
       \<^term>\<open>\<exists>r'[M]. is_converse(M,r,r') \<and> is_domain(M,r',z)\<close>
       unfortunately needs an instance of separation in order to prove
@@ -133,41 +133,41 @@
         \<forall>y[M]. y \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r \<and> (\<exists>x[M]. pair(M,x,y,w)))"
 
 definition
-  is_field :: "[i=>o,i,i] => o" where
+  is_field :: "[i\<Rightarrow>o,i,i] \<Rightarrow> o" where
     "is_field(M,r,z) \<equiv>
         \<exists>dr[M]. \<exists>rr[M]. is_domain(M,r,dr) \<and> is_range(M,r,rr) \<and>
                         union(M,dr,rr,z)"
 
 definition
-  is_relation :: "[i=>o,i] => o" where
+  is_relation :: "[i\<Rightarrow>o,i] \<Rightarrow> o" where
     "is_relation(M,r) \<equiv>
         (\<forall>z[M]. z\<in>r \<longrightarrow> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))"
 
 definition
-  is_function :: "[i=>o,i] => o" where
+  is_function :: "[i\<Rightarrow>o,i] \<Rightarrow> o" where
     "is_function(M,r) \<equiv>
         \<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M].
            pair(M,x,y,p) \<longrightarrow> pair(M,x,y',p') \<longrightarrow> p\<in>r \<longrightarrow> p'\<in>r \<longrightarrow> y=y'"
 
 definition
-  fun_apply :: "[i=>o,i,i,i] => o" where
+  fun_apply :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
     "fun_apply(M,f,x,y) \<equiv>
         (\<exists>xs[M]. \<exists>fxs[M].
          upair(M,x,x,xs) \<and> image(M,f,xs,fxs) \<and> big_union(M,fxs,y))"
 
 definition
-  typed_function :: "[i=>o,i,i,i] => o" where
+  typed_function :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
     "typed_function(M,A,B,r) \<equiv>
         is_function(M,r) \<and> is_relation(M,r) \<and> is_domain(M,r,A) \<and>
         (\<forall>u[M]. u\<in>r \<longrightarrow> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) \<longrightarrow> y\<in>B))"
 
 definition
-  is_funspace :: "[i=>o,i,i,i] => o" where
+  is_funspace :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
     "is_funspace(M,A,B,F) \<equiv>
         \<forall>f[M]. f \<in> F \<longleftrightarrow> typed_function(M,A,B,f)"
 
 definition
-  composition :: "[i=>o,i,i,i] => o" where
+  composition :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
     "composition(M,r,s,t) \<equiv>
         \<forall>p[M]. p \<in> t \<longleftrightarrow>
                (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
@@ -175,104 +175,104 @@
                 xy \<in> s \<and> yz \<in> r)"
 
 definition
-  injection :: "[i=>o,i,i,i] => o" where
+  injection :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
     "injection(M,A,B,f) \<equiv>
         typed_function(M,A,B,f) \<and>
         (\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M].
           pair(M,x,y,p) \<longrightarrow> pair(M,x',y,p') \<longrightarrow> p\<in>f \<longrightarrow> p'\<in>f \<longrightarrow> x=x')"
 
 definition
-  surjection :: "[i=>o,i,i,i] => o" where
+  surjection :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
     "surjection(M,A,B,f) \<equiv>
         typed_function(M,A,B,f) \<and>
         (\<forall>y[M]. y\<in>B \<longrightarrow> (\<exists>x[M]. x\<in>A \<and> fun_apply(M,f,x,y)))"
 
 definition
-  bijection :: "[i=>o,i,i,i] => o" where
+  bijection :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
     "bijection(M,A,B,f) \<equiv> injection(M,A,B,f) \<and> surjection(M,A,B,f)"
 
 definition
-  restriction :: "[i=>o,i,i,i] => o" where
+  restriction :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
     "restriction(M,r,A,z) \<equiv>
         \<forall>x[M]. x \<in> z \<longleftrightarrow> (x \<in> r \<and> (\<exists>u[M]. u\<in>A \<and> (\<exists>v[M]. pair(M,u,v,x))))"
 
 definition
-  transitive_set :: "[i=>o,i] => o" where
+  transitive_set :: "[i\<Rightarrow>o,i] \<Rightarrow> o" where
     "transitive_set(M,a) \<equiv> \<forall>x[M]. x\<in>a \<longrightarrow> subset(M,x,a)"
 
 definition
-  ordinal :: "[i=>o,i] => o" where
+  ordinal :: "[i\<Rightarrow>o,i] \<Rightarrow> o" where
      \<comment> \<open>an ordinal is a transitive set of transitive sets\<close>
     "ordinal(M,a) \<equiv> transitive_set(M,a) \<and> (\<forall>x[M]. x\<in>a \<longrightarrow> transitive_set(M,x))"
 
 definition
-  limit_ordinal :: "[i=>o,i] => o" where
+  limit_ordinal :: "[i\<Rightarrow>o,i] \<Rightarrow> o" where
     \<comment> \<open>a limit ordinal is a non-empty, successor-closed ordinal\<close>
     "limit_ordinal(M,a) \<equiv>
         ordinal(M,a) \<and> \<not> empty(M,a) \<and>
         (\<forall>x[M]. x\<in>a \<longrightarrow> (\<exists>y[M]. y\<in>a \<and> successor(M,x,y)))"
 
 definition
-  successor_ordinal :: "[i=>o,i] => o" where
+  successor_ordinal :: "[i\<Rightarrow>o,i] \<Rightarrow> o" where
     \<comment> \<open>a successor ordinal is any ordinal that is neither empty nor limit\<close>
     "successor_ordinal(M,a) \<equiv>
         ordinal(M,a) \<and> \<not> empty(M,a) \<and> \<not> limit_ordinal(M,a)"
 
 definition
-  finite_ordinal :: "[i=>o,i] => o" where
+  finite_ordinal :: "[i\<Rightarrow>o,i] \<Rightarrow> o" where
     \<comment> \<open>an ordinal is finite if neither it nor any of its elements are limit\<close>
     "finite_ordinal(M,a) \<equiv>
         ordinal(M,a) \<and> \<not> limit_ordinal(M,a) \<and>
         (\<forall>x[M]. x\<in>a \<longrightarrow> \<not> limit_ordinal(M,x))"
 
 definition
-  omega :: "[i=>o,i] => o" where
+  omega :: "[i\<Rightarrow>o,i] \<Rightarrow> o" where
     \<comment> \<open>omega is a limit ordinal none of whose elements are limit\<close>
     "omega(M,a) \<equiv> limit_ordinal(M,a) \<and> (\<forall>x[M]. x\<in>a \<longrightarrow> \<not> limit_ordinal(M,x))"
 
 definition
-  is_quasinat :: "[i=>o,i] => o" where
+  is_quasinat :: "[i\<Rightarrow>o,i] \<Rightarrow> o" where
     "is_quasinat(M,z) \<equiv> empty(M,z) \<or> (\<exists>m[M]. successor(M,m,z))"
 
 definition
-  is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o" where
+  is_nat_case :: "[i\<Rightarrow>o, i, [i,i]\<Rightarrow>o, i, i] \<Rightarrow> o" where
     "is_nat_case(M, a, is_b, k, z) \<equiv>
        (empty(M,k) \<longrightarrow> z=a) \<and>
        (\<forall>m[M]. successor(M,m,k) \<longrightarrow> is_b(m,z)) \<and>
        (is_quasinat(M,k) \<or> empty(M,z))"
 
 definition
-  relation1 :: "[i=>o, [i,i]=>o, i=>i] => o" where
+  relation1 :: "[i\<Rightarrow>o, [i,i]\<Rightarrow>o, i\<Rightarrow>i] \<Rightarrow> o" where
     "relation1(M,is_f,f) \<equiv> \<forall>x[M]. \<forall>y[M]. is_f(x,y) \<longleftrightarrow> y = f(x)"
 
 definition
-  Relation1 :: "[i=>o, i, [i,i]=>o, i=>i] => o" where
+  Relation1 :: "[i\<Rightarrow>o, i, [i,i]\<Rightarrow>o, i\<Rightarrow>i] \<Rightarrow> o" where
     \<comment> \<open>as above, but typed\<close>
     "Relation1(M,A,is_f,f) \<equiv>
         \<forall>x[M]. \<forall>y[M]. x\<in>A \<longrightarrow> is_f(x,y) \<longleftrightarrow> y = f(x)"
 
 definition
-  relation2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o" where
+  relation2 :: "[i\<Rightarrow>o, [i,i,i]\<Rightarrow>o, [i,i]\<Rightarrow>i] \<Rightarrow> o" where
     "relation2(M,is_f,f) \<equiv> \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. is_f(x,y,z) \<longleftrightarrow> z = f(x,y)"
 
 definition
-  Relation2 :: "[i=>o, i, i, [i,i,i]=>o, [i,i]=>i] => o" where
+  Relation2 :: "[i\<Rightarrow>o, i, i, [i,i,i]\<Rightarrow>o, [i,i]\<Rightarrow>i] \<Rightarrow> o" where
     "Relation2(M,A,B,is_f,f) \<equiv>
         \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. x\<in>A \<longrightarrow> y\<in>B \<longrightarrow> is_f(x,y,z) \<longleftrightarrow> z = f(x,y)"
 
 definition
-  relation3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o" where
+  relation3 :: "[i\<Rightarrow>o, [i,i,i,i]\<Rightarrow>o, [i,i,i]\<Rightarrow>i] \<Rightarrow> o" where
     "relation3(M,is_f,f) \<equiv>
        \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. is_f(x,y,z,u) \<longleftrightarrow> u = f(x,y,z)"
 
 definition
-  Relation3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o" where
+  Relation3 :: "[i\<Rightarrow>o, i, i, i, [i,i,i,i]\<Rightarrow>o, [i,i,i]\<Rightarrow>i] \<Rightarrow> o" where
     "Relation3(M,A,B,C,is_f,f) \<equiv>
        \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M].
          x\<in>A \<longrightarrow> y\<in>B \<longrightarrow> z\<in>C \<longrightarrow> is_f(x,y,z,u) \<longleftrightarrow> u = f(x,y,z)"
 
 definition
-  relation4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o" where
+  relation4 :: "[i\<Rightarrow>o, [i,i,i,i,i]\<Rightarrow>o, [i,i,i,i]\<Rightarrow>i] \<Rightarrow> o" where
     "relation4(M,is_f,f) \<equiv>
        \<forall>u[M]. \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>a[M]. is_f(u,x,y,z,a) \<longleftrightarrow> a = f(u,x,y,z)"
 
@@ -290,12 +290,12 @@
 subsection \<open>The relativized ZF axioms\<close>
 
 definition
-  extensionality :: "(i=>o) => o" where
+  extensionality :: "(i\<Rightarrow>o) \<Rightarrow> o" where
     "extensionality(M) \<equiv>
         \<forall>x[M]. \<forall>y[M]. (\<forall>z[M]. z \<in> x \<longleftrightarrow> z \<in> y) \<longrightarrow> x=y"
 
 definition
-  separation :: "[i=>o, i=>o] => o" where
+  separation :: "[i\<Rightarrow>o, i\<Rightarrow>o] \<Rightarrow> o" where
     \<comment> \<open>The formula \<open>P\<close> should only involve parameters
         belonging to \<open>M\<close> and all its quantifiers must be relativized
         to \<open>M\<close>.  We do not have separation as a scheme; every instance
@@ -304,36 +304,36 @@
         \<forall>z[M]. \<exists>y[M]. \<forall>x[M]. x \<in> y \<longleftrightarrow> x \<in> z \<and> P(x)"
 
 definition
-  upair_ax :: "(i=>o) => o" where
+  upair_ax :: "(i\<Rightarrow>o) \<Rightarrow> o" where
     "upair_ax(M) \<equiv> \<forall>x[M]. \<forall>y[M]. \<exists>z[M]. upair(M,x,y,z)"
 
 definition
-  Union_ax :: "(i=>o) => o" where
+  Union_ax :: "(i\<Rightarrow>o) \<Rightarrow> o" where
     "Union_ax(M) \<equiv> \<forall>x[M]. \<exists>z[M]. big_union(M,x,z)"
 
 definition
-  power_ax :: "(i=>o) => o" where
+  power_ax :: "(i\<Rightarrow>o) \<Rightarrow> o" where
     "power_ax(M) \<equiv> \<forall>x[M]. \<exists>z[M]. powerset(M,x,z)"
 
 definition
-  univalent :: "[i=>o, i, [i,i]=>o] => o" where
+  univalent :: "[i\<Rightarrow>o, i, [i,i]\<Rightarrow>o] \<Rightarrow> o" where
     "univalent(M,A,P) \<equiv>
         \<forall>x[M]. x\<in>A \<longrightarrow> (\<forall>y[M]. \<forall>z[M]. P(x,y) \<and> P(x,z) \<longrightarrow> y=z)"
 
 definition
-  replacement :: "[i=>o, [i,i]=>o] => o" where
+  replacement :: "[i\<Rightarrow>o, [i,i]\<Rightarrow>o] \<Rightarrow> o" where
     "replacement(M,P) \<equiv>
       \<forall>A[M]. univalent(M,A,P) \<longrightarrow>
       (\<exists>Y[M]. \<forall>b[M]. (\<exists>x[M]. x\<in>A \<and> P(x,b)) \<longrightarrow> b \<in> Y)"
 
 definition
-  strong_replacement :: "[i=>o, [i,i]=>o] => o" where
+  strong_replacement :: "[i\<Rightarrow>o, [i,i]\<Rightarrow>o] \<Rightarrow> o" where
     "strong_replacement(M,P) \<equiv>
       \<forall>A[M]. univalent(M,A,P) \<longrightarrow>
       (\<exists>Y[M]. \<forall>b[M]. b \<in> Y \<longleftrightarrow> (\<exists>x[M]. x\<in>A \<and> P(x,b)))"
 
 definition
-  foundation_ax :: "(i=>o) => o" where
+  foundation_ax :: "(i\<Rightarrow>o) \<Rightarrow> o" where
     "foundation_ax(M) \<equiv>
         \<forall>x[M]. (\<exists>y[M]. y\<in>x) \<longrightarrow> (\<exists>y[M]. y\<in>x \<and> \<not>(\<exists>z[M]. z\<in>x \<and> z \<in> y))"
 
@@ -360,12 +360,12 @@
 text\<open>Congruence rule for separation: can assume the variable is in \<open>M\<close>\<close>
 lemma separation_cong [cong]:
      "(\<And>x. M(x) \<Longrightarrow> P(x) \<longleftrightarrow> P'(x))
-      \<Longrightarrow> separation(M, %x. P(x)) \<longleftrightarrow> separation(M, %x. P'(x))"
+      \<Longrightarrow> separation(M, \<lambda>x. P(x)) \<longleftrightarrow> separation(M, \<lambda>x. P'(x))"
 by (simp add: separation_def)
 
 lemma univalent_cong [cong]:
      "\<lbrakk>A=A'; \<And>x y. \<lbrakk>x\<in>A; M(x); M(y)\<rbrakk> \<Longrightarrow> P(x,y) \<longleftrightarrow> P'(x,y)\<rbrakk>
-      \<Longrightarrow> univalent(M, A, %x y. P(x,y)) \<longleftrightarrow> univalent(M, A', %x y. P'(x,y))"
+      \<Longrightarrow> univalent(M, A, \<lambda>x y. P(x,y)) \<longleftrightarrow> univalent(M, A', \<lambda>x y. P'(x,y))"
 by (simp add: univalent_def)
 
 lemma univalent_triv [intro,simp]:
@@ -379,8 +379,8 @@
 text\<open>Congruence rule for replacement\<close>
 lemma strong_replacement_cong [cong]:
      "\<lbrakk>\<And>x y. \<lbrakk>M(x); M(y)\<rbrakk> \<Longrightarrow> P(x,y) \<longleftrightarrow> P'(x,y)\<rbrakk>
-      \<Longrightarrow> strong_replacement(M, %x y. P(x,y)) \<longleftrightarrow>
-          strong_replacement(M, %x y. P'(x,y))"
+      \<Longrightarrow> strong_replacement(M, \<lambda>x y. P(x,y)) \<longleftrightarrow>
+          strong_replacement(M, \<lambda>x y. P'(x,y))"
 by (simp add: strong_replacement_def)
 
 text\<open>The extensionality axiom\<close>
@@ -459,13 +459,13 @@
 subsection\<open>Lemmas Needed to Reduce Some Set Constructions to Instances
       of Separation\<close>
 
-lemma image_iff_Collect: "r `` A = {y \<in> \<Union>(\<Union>(r)). \<exists>p\<in>r. \<exists>x\<in>A. p=<x,y>}"
+lemma image_iff_Collect: "r `` A = {y \<in> \<Union>(\<Union>(r)). \<exists>p\<in>r. \<exists>x\<in>A. p=\<langle>x,y\<rangle>}"
 apply (rule equalityI, auto)
 apply (simp add: Pair_def, blast)
 done
 
 lemma vimage_iff_Collect:
-     "r -`` A = {x \<in> \<Union>(\<Union>(r)). \<exists>p\<in>r. \<exists>y\<in>A. p=<x,y>}"
+     "r -`` A = {x \<in> \<Union>(\<Union>(r)). \<exists>p\<in>r. \<exists>y\<in>A. p=\<langle>x,y\<rangle>}"
 apply (rule equalityI, auto)
 apply (simp add: Pair_def, blast)
 done
@@ -503,7 +503,7 @@
 text\<open>More constants, for order types\<close>
 
 definition
-  order_isomorphism :: "[i=>o,i,i,i,i,i] => o" where
+  order_isomorphism :: "[i\<Rightarrow>o,i,i,i,i,i] \<Rightarrow> o" where
     "order_isomorphism(M,A,r,B,s,f) \<equiv>
         bijection(M,A,B,f) \<and>
         (\<forall>x[M]. x\<in>A \<longrightarrow> (\<forall>y[M]. y\<in>A \<longrightarrow>
@@ -512,12 +512,12 @@
             pair(M,fx,fy,q) \<longrightarrow> (p\<in>r \<longleftrightarrow> q\<in>s))))"
 
 definition
-  pred_set :: "[i=>o,i,i,i,i] => o" where
+  pred_set :: "[i\<Rightarrow>o,i,i,i,i] \<Rightarrow> o" where
     "pred_set(M,A,x,r,B) \<equiv>
         \<forall>y[M]. y \<in> B \<longleftrightarrow> (\<exists>p[M]. p\<in>r \<and> y \<in> A \<and> pair(M,y,x,p))"
 
 definition
-  membership :: "[i=>o,i,i] => o" where \<comment> \<open>membership relation\<close>
+  membership :: "[i\<Rightarrow>o,i,i] \<Rightarrow> o" where \<comment> \<open>membership relation\<close>
     "membership(M,A,r) \<equiv>
         \<forall>p[M]. p \<in> r \<longleftrightarrow> (\<exists>x[M]. x\<in>A \<and> (\<exists>y[M]. y\<in>A \<and> x\<in>y \<and> pair(M,x,y,p)))"
 
@@ -628,25 +628,25 @@
   by blast
 
 lemma (in M_trans) pair_abs [simp]:
-     "M(z) \<Longrightarrow> pair(M,a,b,z) \<longleftrightarrow> z=<a,b>"
+     "M(z) \<Longrightarrow> pair(M,a,b,z) \<longleftrightarrow> z=\<langle>a,b\<rangle>"
 apply (simp add: pair_def Pair_def)
 apply (blast intro: transM)
 done
 
 lemma (in M_trans) pair_in_MD [dest!]:
-     "M(<a,b>) \<Longrightarrow> M(a) \<and> M(b)"
+     "M(\<langle>a,b\<rangle>) \<Longrightarrow> M(a) \<and> M(b)"
   by (simp add: Pair_def, blast intro: transM)
 
 lemma (in M_trivial) pair_in_MI [intro!]:
-     "M(a) \<and> M(b) \<Longrightarrow> M(<a,b>)"
+     "M(a) \<and> M(b) \<Longrightarrow> M(\<langle>a,b\<rangle>)"
   by (simp add: Pair_def)
 
 lemma (in M_trivial) pair_in_M_iff [simp]:
-     "M(<a,b>) \<longleftrightarrow> M(a) \<and> M(b)"
+     "M(\<langle>a,b\<rangle>) \<longleftrightarrow> M(a) \<and> M(b)"
   by blast
 
 lemma (in M_trans) pair_components_in_M:
-     "\<lbrakk><x,y> \<in> A; M(A)\<rbrakk> \<Longrightarrow> M(x) \<and> M(y)"
+     "\<lbrakk>\<langle>x,y\<rangle> \<in> A; M(A)\<rbrakk> \<Longrightarrow> M(x) \<and> M(y)"
   by (blast dest: transM)
 
 lemma (in M_trivial) cartprod_abs [simp]:
@@ -739,8 +739,8 @@
      "\<lbrakk>A=A';
          \<And>x y. \<lbrakk>M(x); M(y)\<rbrakk> \<Longrightarrow> P(x,y) \<longleftrightarrow> P'(x,y);
          z=z'\<rbrakk>
-      \<Longrightarrow> is_Replace(M, A, %x y. P(x,y), z) \<longleftrightarrow>
-          is_Replace(M, A', %x y. P'(x,y), z')"
+      \<Longrightarrow> is_Replace(M, A, \<lambda>x y. P(x,y), z) \<longleftrightarrow>
+          is_Replace(M, A', \<lambda>x y. P'(x,y), z')"
 by (simp add: is_Replace_def)
 
 lemma (in M_trans) univalent_Replace_iff:
@@ -795,7 +795,7 @@
       makes relativization easier.\<close>
 lemma (in M_trans) RepFun_closed2:
      "\<lbrakk>strong_replacement(M, \<lambda>x y. x\<in>A \<and> y = f(x)); M(A); \<forall>x\<in>A. M(f(x))\<rbrakk>
-      \<Longrightarrow> M(RepFun(A, %x. f(x)))"
+      \<Longrightarrow> M(RepFun(A, \<lambda>x. f(x)))"
 apply (simp add: RepFun_def)
 apply (frule strong_replacement_closed, assumption)
 apply (auto dest: transM  simp add: Replace_conj_eq univalent_def)
@@ -804,7 +804,7 @@
 subsubsection \<open>Absoluteness for \<^term>\<open>Lambda\<close>\<close>
 
 definition
- is_lambda :: "[i=>o, i, [i,i]=>o, i] => o" where
+ is_lambda :: "[i\<Rightarrow>o, i, [i,i]\<Rightarrow>o, i] \<Rightarrow> o" where
     "is_lambda(M, A, is_b, z) \<equiv>
        \<forall>p[M]. p \<in> z \<longleftrightarrow>
         (\<exists>u[M]. \<exists>v[M]. u\<in>A \<and> pair(M,u,v,p) \<and> is_b(u,v))"
@@ -838,8 +838,8 @@
 lemma is_lambda_cong [cong]:
      "\<lbrakk>A=A';  z=z';
          \<And>x y. \<lbrakk>x\<in>A; M(x); M(y)\<rbrakk> \<Longrightarrow> is_b(x,y) \<longleftrightarrow> is_b'(x,y)\<rbrakk>
-      \<Longrightarrow> is_lambda(M, A, %x y. is_b(x,y), z) \<longleftrightarrow>
-          is_lambda(M, A', %x y. is_b'(x,y), z')"
+      \<Longrightarrow> is_lambda(M, A, \<lambda>x y. is_b(x,y), z) \<longleftrightarrow>
+          is_lambda(M, A', \<lambda>x y. is_b'(x,y), z')"
 by (simp add: is_lambda_def)
 
 lemma (in M_trans) image_abs [simp]:
@@ -1001,7 +1001,7 @@
   equations only hold for x\<in>nat (or in some other set) and not for the
   whole of the class M.
   consts
-    natnumber_aux :: "[i=>o,i] => i"
+    natnumber_aux :: "[i\<Rightarrow>o,i] \<Rightarrow> i"
 
   primrec
       "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"
@@ -1010,7 +1010,7 @@
                      then 1 else 0)"
 
   definition
-    natnumber :: "[i=>o,i,i] => o"
+    natnumber :: "[i\<Rightarrow>o,i,i] \<Rightarrow> o"
       "natnumber(M,n,x) \<equiv> natnumber_aux(M,n)`x = 1"
 
   lemma (in M_trivial) [simp]:
@@ -1076,7 +1076,7 @@
      "\<lbrakk>M(A); M(B); M(C)\<rbrakk>
       \<Longrightarrow> cartprod(M,A,B,C) \<longleftrightarrow>
           (\<exists>p1[M]. \<exists>p2[M]. powerset(M,A \<union> B,p1) \<and> powerset(M,p1,p2) \<and>
-                   C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})"
+                   C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = \<langle>x,y\<rangle>})"
 apply (simp add: Pair_def cartprod_def, safe)
 defer 1
   apply (simp add: powerset_def)
@@ -1348,15 +1348,15 @@
 
 (*???equalities*)
 lemma Collect_Un_Collect_eq:
-     "Collect(A,P) \<union> Collect(A,Q) = Collect(A, %x. P(x) \<or> Q(x))"
+     "Collect(A,P) \<union> Collect(A,Q) = Collect(A, \<lambda>x. P(x) \<or> Q(x))"
 by blast
 
 lemma Diff_Collect_eq:
-     "A - Collect(A,P) = Collect(A, %x. \<not> P(x))"
+     "A - Collect(A,P) = Collect(A, \<lambda>x. \<not> P(x))"
 by blast
 
 lemma (in M_trans) Collect_rall_eq:
-     "M(Y) \<Longrightarrow> Collect(A, %x. \<forall>y[M]. y\<in>Y \<longrightarrow> P(x,y)) =
+     "M(Y) \<Longrightarrow> Collect(A, \<lambda>x. \<forall>y[M]. y\<in>Y \<longrightarrow> P(x,y)) =
                (if Y=0 then A else (\<Inter>y \<in> Y. {x \<in> A. P(x,y)}))"
   by (simp,blast dest: transM)
 
@@ -1405,7 +1405,7 @@
 lemma (in M_basic) succ_fun_eq2:
      "\<lbrakk>M(B); M(n->B)\<rbrakk> \<Longrightarrow>
       succ(n) -> B =
-      \<Union>{z. p \<in> (n->B)*B, \<exists>f[M]. \<exists>b[M]. p = <f,b> \<and> z = {cons(<n,b>, f)}}"
+      \<Union>{z. p \<in> (n->B)*B, \<exists>f[M]. \<exists>b[M]. p = \<langle>f,b\<rangle> \<and> z = {cons(\<langle>n,b\<rangle>, f)}}"
 apply (simp add: succ_fun_eq)
 apply (blast dest: transM)
 done
@@ -1429,21 +1429,21 @@
 subsection\<open>Relativization and Absoluteness for Boolean Operators\<close>
 
 definition
-  is_bool_of_o :: "[i=>o, o, i] => o" where
+  is_bool_of_o :: "[i\<Rightarrow>o, o, i] \<Rightarrow> o" where
    "is_bool_of_o(M,P,z) \<equiv> (P \<and> number1(M,z)) \<or> (\<not>P \<and> empty(M,z))"
 
 definition
-  is_not :: "[i=>o, i, i] => o" where
+  is_not :: "[i\<Rightarrow>o, i, i] \<Rightarrow> o" where
    "is_not(M,a,z) \<equiv> (number1(M,a)  \<and> empty(M,z)) |
                      (\<not>number1(M,a) \<and> number1(M,z))"
 
 definition
-  is_and :: "[i=>o, i, i, i] => o" where
+  is_and :: "[i\<Rightarrow>o, i, i, i] \<Rightarrow> o" where
    "is_and(M,a,b,z) \<equiv> (number1(M,a)  \<and> z=b) |
                        (\<not>number1(M,a) \<and> empty(M,z))"
 
 definition
-  is_or :: "[i=>o, i, i, i] => o" where
+  is_or :: "[i\<Rightarrow>o, i, i, i] \<Rightarrow> o" where
    "is_or(M,a,b,z) \<equiv> (number1(M,a)  \<and> number1(M,z)) |
                       (\<not>number1(M,a) \<and> z=b)"
 
@@ -1485,12 +1485,12 @@
 subsection\<open>Relativization and Absoluteness for List Operators\<close>
 
 definition
-  is_Nil :: "[i=>o, i] => o" where
+  is_Nil :: "[i\<Rightarrow>o, i] \<Rightarrow> o" where
      \<comment> \<open>because \<^prop>\<open>[] \<equiv> Inl(0)\<close>\<close>
     "is_Nil(M,xs) \<equiv> \<exists>zero[M]. empty(M,zero) \<and> is_Inl(M,zero,xs)"
 
 definition
-  is_Cons :: "[i=>o,i,i,i] => o" where
+  is_Cons :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
      \<comment> \<open>because \<^prop>\<open>Cons(a, l) \<equiv> Inr(\<langle>a,l\<rangle>)\<close>\<close>
     "is_Cons(M,a,l,Z) \<equiv> \<exists>p[M]. pair(M,a,l,p) \<and> is_Inr(M,p,Z)"
 
@@ -1510,21 +1510,21 @@
 
 
 definition
-  quasilist :: "i => o" where
+  quasilist :: "i \<Rightarrow> o" where
     "quasilist(xs) \<equiv> xs=Nil \<or> (\<exists>x l. xs = Cons(x,l))"
 
 definition
-  is_quasilist :: "[i=>o,i] => o" where
+  is_quasilist :: "[i\<Rightarrow>o,i] \<Rightarrow> o" where
     "is_quasilist(M,z) \<equiv> is_Nil(M,z) \<or> (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))"
 
 definition
-  list_case' :: "[i, [i,i]=>i, i] => i" where
+  list_case' :: "[i, [i,i]\<Rightarrow>i, i] \<Rightarrow> i" where
     \<comment> \<open>A version of \<^term>\<open>list_case\<close> that's always defined.\<close>
     "list_case'(a,b,xs) \<equiv>
        if quasilist(xs) then list_case(a,b,xs) else 0"
 
 definition
-  is_list_case :: "[i=>o, i, [i,i,i]=>o, i, i] => o" where
+  is_list_case :: "[i\<Rightarrow>o, i, [i,i,i]\<Rightarrow>o, i, i] \<Rightarrow> o" where
     \<comment> \<open>Returns 0 for non-lists\<close>
     "is_list_case(M, a, is_b, xs, z) \<equiv>
        (is_Nil(M,xs) \<longrightarrow> z=a) \<and>
@@ -1532,17 +1532,17 @@
        (is_quasilist(M,xs) \<or> empty(M,z))"
 
 definition
-  hd' :: "i => i" where
+  hd' :: "i \<Rightarrow> i" where
     \<comment> \<open>A version of \<^term>\<open>hd\<close> that's always defined.\<close>
     "hd'(xs) \<equiv> if quasilist(xs) then hd(xs) else 0"
 
 definition
-  tl' :: "i => i" where
+  tl' :: "i \<Rightarrow> i" where
     \<comment> \<open>A version of \<^term>\<open>tl\<close> that's always defined.\<close>
     "tl'(xs) \<equiv> if quasilist(xs) then tl(xs) else 0"
 
 definition
-  is_hd :: "[i=>o,i,i] => o" where
+  is_hd :: "[i\<Rightarrow>o,i,i] \<Rightarrow> o" where
      \<comment> \<open>\<^term>\<open>hd([]) = 0\<close> no constraints if not a list.
           Avoiding implication prevents the simplifier's looping.\<close>
     "is_hd(M,xs,H) \<equiv>
@@ -1551,7 +1551,7 @@
        (is_quasilist(M,xs) \<or> empty(M,H))"
 
 definition
-  is_tl :: "[i=>o,i,i] => o" where
+  is_tl :: "[i\<Rightarrow>o,i,i] \<Rightarrow> o" where
      \<comment> \<open>\<^term>\<open>tl([]) = []\<close>; see comments about \<^term>\<open>is_hd\<close>\<close>
     "is_tl(M,xs,T) \<equiv>
        (is_Nil(M,xs) \<longrightarrow> T=xs) \<and>