src/HOL/Lambda/Lambda.thy

 
 lemma subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j"
   apply (simp add: subst_Var)
   done
 
-lemma lift_lift [rulified]:
+lemma lift_lift [rule_format]:
     "\<forall>i k. i < k + 1 --> lift (lift t i) (Suc k) = lift (lift t k) i"
   apply (induct_tac t)
     apply auto
   done
 

     "\<forall>k s. (lift t k)[s/k] = t"
   apply (induct_tac t)
     apply simp_all
   done
 
-lemma subst_subst [rulified]:
+lemma subst_subst [rule_format]:
     "\<forall>i j u v. i < j + 1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
   apply (induct_tac t)
     apply (simp_all
       add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
       split: nat.split)

 subsection {* Preservation theorems *}
 
 text {* Not used in Church-Rosser proof, but in Strong
   Normalization. \medskip *}
 
-theorem subst_preserves_beta [rulified, simp]:
+theorem subst_preserves_beta [rule_format, simp]:
     "r -> s ==> \<forall>t i. r[t/i] -> s[t/i]"
   apply (erule beta.induct)
      apply (simp_all add: subst_subst [symmetric])
   done
 
-theorem lift_preserves_beta [rulified, simp]:
+theorem lift_preserves_beta [rule_format, simp]:
     "r -> s ==> \<forall>i. lift r i -> lift s i"
   apply (erule beta.induct)
      apply auto
   done
 
-theorem subst_preserves_beta2 [rulified, simp]:
+theorem subst_preserves_beta2 [rule_format, simp]:
     "\<forall>r s i. r -> s --> t[r/i] ->> t[s/i]"
   apply (induct_tac t)
     apply (simp add: subst_Var r_into_rtrancl)
    apply (simp add: rtrancl_beta_App)
   apply (simp add: rtrancl_beta_Abs)