src/HOL/Isar_Examples/Nested_Datatype.thy

 begin
 
 subsection {* Terms and substitution *}
 
 datatype ('a, 'b) "term" =
-    Var 'a
-  | App 'b "('a, 'b) term list"
+  Var 'a
+| App 'b "('a, 'b) term list"
 
-primrec
-  subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" and
-  subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
+primrec subst_term :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term \<Rightarrow> ('a, 'b) term"
+  and subst_term_list :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term list \<Rightarrow> ('a, 'b) term list"
 where
   "subst_term f (Var a) = f a"
 | "subst_term f (App b ts) = App b (subst_term_list f ts)"
 | "subst_term_list f [] = []"
 | "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"

 lemmas subst_simps = subst_term_subst_term_list.simps
 
 text {* \medskip A simple lemma about composition of substitutions. *}
 
 lemma
-  "subst_term (subst_term f1 o f2) t =
+  "subst_term (subst_term f1 \<circ> f2) t =
     subst_term f1 (subst_term f2 t)"
   and
-  "subst_term_list (subst_term f1 o f2) ts =
+  "subst_term_list (subst_term f1 \<circ> f2) ts =
     subst_term_list f1 (subst_term_list f2 ts)"
   by (induct t and ts) simp_all
 
-lemma "subst_term (subst_term f1 o f2) t =
+lemma "subst_term (subst_term f1 \<circ> f2) t =
     subst_term f1 (subst_term f2 t)"
 proof -
   let "?P t" = ?thesis
-  let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 o f2) ts =
+  let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 \<circ> f2) ts =
     subst_term_list f1 (subst_term_list f2 ts)"
   show ?thesis
   proof (induct t)
     fix a show "?P (Var a)" by simp
   next

 
 
 subsection {* Alternative induction *}
 
 theorem term_induct' [case_names Var App]:
-  assumes var: "!!a. P (Var a)"
-    and app: "!!b ts. (\<forall>t \<in> set ts. P t) ==> P (App b ts)"
+  assumes var: "\<And>a. P (Var a)"
+    and app: "\<And>b ts. (\<forall>t \<in> set ts. P t) \<Longrightarrow> P (App b ts)"
   shows "P t"
 proof (induct t)
   fix a show "P (Var a)" by (rule var)
 next
   fix b t ts assume "\<forall>t \<in> set ts. P t"

 next
   fix t ts assume "P t" "\<forall>t' \<in> set ts. P t'"
   then show "\<forall>t' \<in> set (t # ts). P t'" by simp
 qed
 
-lemma
-  "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
+lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)"
 proof (induct t rule: term_induct')
   case (Var a)
   show ?case by (simp add: o_def)
 next
   case (App b ts)