src/HOL/Lambda/InductTermi.thy

     Var [intro]: "listsp IT rs ==> IT (Var n \<degree>\<degree> rs)"
   | Lambda [intro]: "IT r ==> IT (Abs r)"
   | Beta [intro]: "IT ((r[s/0]) \<degree>\<degree> ss) ==> IT s ==> IT ((Abs r \<degree> s) \<degree>\<degree> ss)"
 
 
-subsection {* Every term in IT terminates *}
+subsection {* Every term in @{text "IT"} terminates *}
 
 lemma double_induction_lemma [rule_format]:
   "termip beta s ==> \<forall>t. termip beta t -->
     (\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> termip beta (Abs r \<degree> s \<degree>\<degree> ss))"
   apply (erule accp_induct)

    apply blast
   apply (blast intro: double_induction_lemma)
   done
 
 
-subsection {* Every terminating term is in IT *}
+subsection {* Every terminating term is in @{text "IT"} *}
 
 declare Var_apps_neq_Abs_apps [symmetric, simp]
 
 lemma [simp, THEN not_sym, simp]: "Var n \<degree>\<degree> ss \<noteq> Abs r \<degree> s \<degree>\<degree> ts"
   by (simp add: foldl_Cons [symmetric] del: foldl_Cons)