src/HOL/Lambda/ParRed.thy
changeset 9906 5c027cca6262
parent 9811 39ffdb8cab03
child 9941 fe05af7ec816
     1.1 --- a/src/HOL/Lambda/ParRed.thy	Thu Sep 07 21:06:55 2000 +0200
     1.2 +++ b/src/HOL/Lambda/ParRed.thy	Thu Sep 07 21:10:11 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 [rulify, simp]:
     1.8 +lemma par_beta_lift [rulified, 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 [rulify]:
    1.15 +lemma par_beta_subst [rulified]:
    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 [rulify]:
    1.24 +lemma par_beta_cd [rulified]:
    1.25      "\<forall>t. s => t --> t => cd s"
    1.26    apply (induct_tac s rule: cd.induct)
    1.27        apply auto