diff -r f2094906e491 -r e44d86131648 src/ZF/Induct/Binary_Trees.thy
--- a/src/ZF/Induct/Binary_Trees.thy	Tue Sep 27 13:34:54 2022 +0200
+++ b/src/ZF/Induct/Binary_Trees.thy	Tue Sep 27 16:51:35 2022 +0100
@@ -17,7 +17,7 @@
 
 declare bt.intros [simp]
 
-lemma Br_neq_left: "l \<in> bt(A) ==> Br(x, l, r) \<noteq> l"
+lemma Br_neq_left: "l \<in> bt(A) \<Longrightarrow> Br(x, l, r) \<noteq> l"
   by (induct arbitrary: x r set: bt) auto
 
 lemma Br_iff: "Br(a, l, r) = Br(a', l', r') \<longleftrightarrow> a = a' & l = l' & r = r'"
@@ -32,7 +32,7 @@
   definitions.
 \<close>
 
-lemma bt_mono: "A \<subseteq> B ==> bt(A) \<subseteq> bt(B)"
+lemma bt_mono: "A \<subseteq> B \<Longrightarrow> bt(A) \<subseteq> bt(B)"
   apply (unfold bt.defs)
   apply (rule lfp_mono)
     apply (rule bt.bnd_mono)+
@@ -46,18 +46,18 @@
   apply (fast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ)
   done
 
-lemma bt_subset_univ: "A \<subseteq> univ(B) ==> bt(A) \<subseteq> univ(B)"
+lemma bt_subset_univ: "A \<subseteq> univ(B) \<Longrightarrow> bt(A) \<subseteq> univ(B)"
   apply (rule subset_trans)
    apply (erule bt_mono)
   apply (rule bt_univ)
   done
 
 lemma bt_rec_type:
-  "[| t \<in> bt(A);
+  "\<lbrakk>t \<in> bt(A);
     c \<in> C(Lf);
-    !!x y z r s. [| x \<in> A;  y \<in> bt(A);  z \<in> bt(A);  r \<in> C(y);  s \<in> C(z) |] ==>
+    \<And>x y z r s. \<lbrakk>x \<in> A;  y \<in> bt(A);  z \<in> bt(A);  r \<in> C(y);  s \<in> C(z)\<rbrakk> \<Longrightarrow>
     h(x, y, z, r, s) \<in> C(Br(x, y, z))
-  |] ==> bt_rec(c, h, t) \<in> C(t)"
+\<rbrakk> \<Longrightarrow> bt_rec(c, h, t) \<in> C(t)"
   \<comment> \<open>Type checking for recursor -- example only; not really needed.\<close>
   apply (induct_tac t)
    apply simp_all
@@ -71,7 +71,7 @@
   "n_nodes(Lf) = 0"
   "n_nodes(Br(a, l, r)) = succ(n_nodes(l) #+ n_nodes(r))"
 
-lemma n_nodes_type [simp]: "t \<in> bt(A) ==> n_nodes(t) \<in> nat"
+lemma n_nodes_type [simp]: "t \<in> bt(A) \<Longrightarrow> n_nodes(t) \<in> nat"
   by (induct set: bt) auto
 
 consts  n_nodes_aux :: "i => i"
@@ -81,7 +81,7 @@
       (\<lambda>k \<in> nat. n_nodes_aux(r) `  (n_nodes_aux(l) ` succ(k)))"
 
 lemma n_nodes_aux_eq:
-    "t \<in> bt(A) ==> k \<in> nat ==> n_nodes_aux(t)`k = n_nodes(t) #+ k"
+    "t \<in> bt(A) \<Longrightarrow> k \<in> nat \<Longrightarrow> n_nodes_aux(t)`k = n_nodes(t) #+ k"
   apply (induct arbitrary: k set: bt)
    apply simp
   apply (atomize, simp)
@@ -89,9 +89,9 @@
 
 definition
   n_nodes_tail :: "i => i"  where
-  "n_nodes_tail(t) == n_nodes_aux(t) ` 0"
+  "n_nodes_tail(t) \<equiv> n_nodes_aux(t) ` 0"
 
-lemma "t \<in> bt(A) ==> n_nodes_tail(t) = n_nodes(t)"
+lemma "t \<in> bt(A) \<Longrightarrow> n_nodes_tail(t) = n_nodes(t)"
   by (simp add: n_nodes_tail_def n_nodes_aux_eq)
 
 
@@ -103,7 +103,7 @@
   "n_leaves(Lf) = 1"
   "n_leaves(Br(a, l, r)) = n_leaves(l) #+ n_leaves(r)"
 
-lemma n_leaves_type [simp]: "t \<in> bt(A) ==> n_leaves(t) \<in> nat"
+lemma n_leaves_type [simp]: "t \<in> bt(A) \<Longrightarrow> n_leaves(t) \<in> nat"
   by (induct set: bt) auto
 
 
@@ -115,24 +115,24 @@
   "bt_reflect(Lf) = Lf"
   "bt_reflect(Br(a, l, r)) = Br(a, bt_reflect(r), bt_reflect(l))"
 
-lemma bt_reflect_type [simp]: "t \<in> bt(A) ==> bt_reflect(t) \<in> bt(A)"
+lemma bt_reflect_type [simp]: "t \<in> bt(A) \<Longrightarrow> bt_reflect(t) \<in> bt(A)"
   by (induct set: bt) auto
 
 text \<open>
   \medskip Theorems about \<^term>\<open>n_leaves\<close>.
 \<close>
 
-lemma n_leaves_reflect: "t \<in> bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)"
+lemma n_leaves_reflect: "t \<in> bt(A) \<Longrightarrow> n_leaves(bt_reflect(t)) = n_leaves(t)"
   by (induct set: bt) (simp_all add: add_commute)
 
-lemma n_leaves_nodes: "t \<in> bt(A) ==> n_leaves(t) = succ(n_nodes(t))"
+lemma n_leaves_nodes: "t \<in> bt(A) \<Longrightarrow> n_leaves(t) = succ(n_nodes(t))"
   by (induct set: bt) simp_all
 
 text \<open>
   Theorems about \<^term>\<open>bt_reflect\<close>.
 \<close>
 
-lemma bt_reflect_bt_reflect_ident: "t \<in> bt(A) ==> bt_reflect(bt_reflect(t)) = t"
+lemma bt_reflect_bt_reflect_ident: "t \<in> bt(A) \<Longrightarrow> bt_reflect(bt_reflect(t)) = t"
   by (induct set: bt) simp_all
 
 end