src/HOL/Lambda/ParRed.thy
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 11638 2c3dee321b4b
     1.1 --- a/src/HOL/Lambda/ParRed.thy	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/src/HOL/Lambda/ParRed.thy	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -70,13 +70,13 @@
     1.4  
     1.5  subsection {* Misc properties of par-beta *}
     1.6  
     1.7 -lemma par_beta_lift [rulified, simp]:
     1.8 +lemma par_beta_lift [rule_format, simp]:
     1.9      "\<forall>t' n. t => t' --> lift t n => lift t' n"
    1.10    apply (induct_tac t)
    1.11      apply fastsimp+
    1.12    done
    1.13  
    1.14 -lemma par_beta_subst [rulified]:
    1.15 +lemma par_beta_subst [rule_format]:
    1.16      "\<forall>s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]"
    1.17    apply (induct_tac t)
    1.18      apply (simp add: subst_Var)
    1.19 @@ -110,7 +110,7 @@
    1.20    "cd (Abs u $ t) = (cd u)[cd t/0]"
    1.21    "cd (Abs s) = Abs (cd s)"
    1.22  
    1.23 -lemma par_beta_cd [rulified]:
    1.24 +lemma par_beta_cd [rule_format]:
    1.25      "\<forall>t. s => t --> t => cd s"
    1.26    apply (induct_tac s rule: cd.induct)
    1.27        apply auto