src/HOL/Lambda/Eta.thy
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 11183 0476c6e07bca
     1.1 --- a/src/HOL/Lambda/Eta.thy	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/src/HOL/Lambda/Eta.thy	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -45,7 +45,7 @@
     1.4  
     1.5  subsection "Properties of eta, subst and free"
     1.6  
     1.7 -lemma subst_not_free [rulified, simp]:
     1.8 +lemma subst_not_free [rule_format, simp]:
     1.9      "\<forall>i t u. \<not> free s i --> s[t/i] = s[u/i]"
    1.10    apply (induct_tac s)
    1.11      apply (simp_all add: subst_Var)
    1.12 @@ -74,7 +74,7 @@
    1.13    apply simp_all
    1.14    done
    1.15  
    1.16 -lemma free_eta [rulified]:
    1.17 +lemma free_eta [rule_format]:
    1.18      "s -e> t ==> \<forall>i. free t i = free s i"
    1.19    apply (erule eta.induct)
    1.20       apply (simp_all cong: conj_cong)
    1.21 @@ -85,7 +85,7 @@
    1.22    apply (simp add: free_eta)
    1.23    done
    1.24  
    1.25 -lemma eta_subst [rulified, simp]:
    1.26 +lemma eta_subst [rule_format, simp]:
    1.27      "s -e> t ==> \<forall>u i. s[u/i] -e> t[u/i]"
    1.28    apply (erule eta.induct)
    1.29    apply (simp_all add: subst_subst [symmetric])
    1.30 @@ -136,13 +136,13 @@
    1.31  
    1.32  subsection "Commutation of beta and eta"
    1.33  
    1.34 -lemma free_beta [rulified]:
    1.35 +lemma free_beta [rule_format]:
    1.36      "s -> t ==> \<forall>i. free t i --> free s i"
    1.37    apply (erule beta.induct)
    1.38       apply simp_all
    1.39    done
    1.40  
    1.41 -lemma beta_subst [rulified, intro]:
    1.42 +lemma beta_subst [rule_format, intro]:
    1.43      "s -> t ==> \<forall>u i. s[u/i] -> t[u/i]"
    1.44    apply (erule beta.induct)
    1.45       apply (simp_all add: subst_subst [symmetric])
    1.46 @@ -153,13 +153,13 @@
    1.47    apply (auto elim!: linorder_neqE simp: subst_Var)
    1.48    done
    1.49  
    1.50 -lemma eta_lift [rulified, simp]:
    1.51 +lemma eta_lift [rule_format, simp]:
    1.52      "s -e> t ==> \<forall>i. lift s i -e> lift t i"
    1.53    apply (erule eta.induct)
    1.54       apply simp_all
    1.55    done
    1.56  
    1.57 -lemma rtrancl_eta_subst [rulified]:
    1.58 +lemma rtrancl_eta_subst [rule_format]:
    1.59      "\<forall>s t i. s -e> t --> u[s/i] -e>> u[t/i]"
    1.60    apply (induct_tac u)
    1.61      apply (simp_all add: subst_Var)
    1.62 @@ -190,7 +190,7 @@
    1.63  
    1.64  text {* @{term "Abs (lift s 0 $ Var 0) -e> s"} *}
    1.65  
    1.66 -lemma not_free_iff_lifted [rulified]:
    1.67 +lemma not_free_iff_lifted [rule_format]:
    1.68      "\<forall>i. (\<not> free s i) = (\<exists>t. s = lift t i)"
    1.69    apply (induct_tac s)
    1.70      apply simp