src/HOL/Lambda/Lambda.thy
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 10851 31ac62e3a0ed
     1.1 --- a/src/HOL/Lambda/Lambda.thy	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/src/HOL/Lambda/Lambda.thy	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -120,7 +120,7 @@
     1.4    apply (simp add: subst_Var)
     1.5    done
     1.6  
     1.7 -lemma lift_lift [rulified]:
     1.8 +lemma lift_lift [rule_format]:
     1.9      "\<forall>i k. i < k + 1 --> lift (lift t i) (Suc k) = lift (lift t k) i"
    1.10    apply (induct_tac t)
    1.11      apply auto
    1.12 @@ -144,7 +144,7 @@
    1.13      apply simp_all
    1.14    done
    1.15  
    1.16 -lemma subst_subst [rulified]:
    1.17 +lemma subst_subst [rule_format]:
    1.18      "\<forall>i j u v. i < j + 1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
    1.19    apply (induct_tac t)
    1.20      apply (simp_all
    1.21 @@ -183,19 +183,19 @@
    1.22  text {* Not used in Church-Rosser proof, but in Strong
    1.23    Normalization. \medskip *}
    1.24  
    1.25 -theorem subst_preserves_beta [rulified, simp]:
    1.26 +theorem subst_preserves_beta [rule_format, simp]:
    1.27      "r -> s ==> \<forall>t i. r[t/i] -> s[t/i]"
    1.28    apply (erule beta.induct)
    1.29       apply (simp_all add: subst_subst [symmetric])
    1.30    done
    1.31  
    1.32 -theorem lift_preserves_beta [rulified, simp]:
    1.33 +theorem lift_preserves_beta [rule_format, simp]:
    1.34      "r -> s ==> \<forall>i. lift r i -> lift s i"
    1.35    apply (erule beta.induct)
    1.36       apply auto
    1.37    done
    1.38  
    1.39 -theorem subst_preserves_beta2 [rulified, simp]:
    1.40 +theorem subst_preserves_beta2 [rule_format, simp]:
    1.41      "\<forall>r s i. r -> s --> t[r/i] ->> t[s/i]"
    1.42    apply (induct_tac t)
    1.43      apply (simp add: subst_Var r_into_rtrancl)