src/HOL/Lambda/Type.thy

--- a/src/HOL/Lambda/Type.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Lambda/Type.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -74,7 +74,7 @@
 
 text {* Iterated function types *}
 
-lemma list_app_typeD [rulify]:
+lemma list_app_typeD [rulified]:
     "\<forall>t T. e |- t $$ ts : T --> (\<exists>Ts. e |- t : Ts =>> T \<and> types e ts Ts)"
   apply (induct_tac ts)
    apply simp
@@ -90,7 +90,7 @@
   apply simp
   done
 
-lemma list_app_typeI [rulify]:
+lemma list_app_typeI [rulified]:
     "\<forall>t T Ts. e |- t : Ts =>> T --> types e ts Ts --> e |- t $$ ts : T"
   apply (induct_tac ts)
    apply (intro strip)
@@ -109,7 +109,7 @@
   apply blast
   done
 
-lemma lists_types [rulify]:
+lemma lists_types [rulified]:
     "\<forall>Ts. types e ts Ts --> ts \<in> lists {t. \<exists>T. e |- t : T}"
   apply (induct_tac ts)
    apply (intro strip)
@@ -129,19 +129,19 @@
 
 subsection {* Lifting preserves termination and well-typedness *}
 
-lemma lift_map [rulify, simp]:
+lemma lift_map [rulified, simp]:
     "\<forall>t. lift (t $$ ts) i = lift t i $$ map (\<lambda>t. lift t i) ts"
   apply (induct_tac ts)
    apply simp_all
   done
 
-lemma subst_map [rulify, simp]:
+lemma subst_map [rulified, simp]:
   "\<forall>t. subst (t $$ ts) u i = subst t u i $$ map (\<lambda>t. subst t u i) ts"
   apply (induct_tac ts)
    apply simp_all
   done
 
-lemma lift_IT [rulify, intro!]:
+lemma lift_IT [rulified, intro!]:
     "t \<in> IT ==> \<forall>i. lift t i \<in> IT"
   apply (erule IT.induct)
     apply (rule allI)
@@ -161,7 +161,7 @@
      apply auto
    done
 
-lemma lifts_IT [rulify]:
+lemma lifts_IT [rulified]:
     "ts \<in> lists IT --> map (\<lambda>t. lift t 0) ts \<in> lists IT"
   apply (induct_tac ts)
    apply auto
@@ -180,7 +180,7 @@
    apply simp_all
   done
 
-lemma lift_type' [rulify]:
+lemma lift_type' [rulified]:
   "e |- t : T ==> \<forall>i U.
     (\<lambda>j. if j < i then e j
           else if j = i then U
@@ -202,7 +202,7 @@
    apply simp_all
   done
 
-lemma lift_types [rulify]:
+lemma lift_types [rulified]:
   "\<forall>Ts. types e ts Ts -->
     types (\<lambda>j. if j < i then e j
                 else if j = i then U
@@ -219,7 +219,7 @@
 
 subsection {* Substitution lemmas *}
 
-lemma subst_lemma [rulify]:
+lemma subst_lemma [rulified]:
   "e |- t : T ==> \<forall>e' i U u.
     e = (\<lambda>j. if j < i then e' j
               else if j = i then U
@@ -242,7 +242,7 @@
   apply fastsimp
   done
 
-lemma substs_lemma [rulify]:
+lemma substs_lemma [rulified]:
   "e |- u : T ==>
     \<forall>Ts. types (\<lambda>j. if j < i then e j
                      else if j = i then T else e (j - 1)) ts Ts -->
@@ -265,7 +265,7 @@
 
 subsection {* Subject reduction *}
 
-lemma subject_reduction [rulify]:
+lemma subject_reduction [rulified]:
     "e |- t : T ==> \<forall>t'. t -> t' --> e |- t' : T"
   apply (erule typing.induct)
     apply blast
@@ -290,7 +290,7 @@
   apply simp
   done
 
-lemma subst_Var_IT [rulify]: "r \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT"
+lemma subst_Var_IT [rulified]: "r \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT"
   apply (erule IT.induct)
     txt {* Case @{term Var}: *}
     apply (intro strip)
@@ -334,7 +334,7 @@
     apply (rule lists.Cons)
      apply (rule Var_IT)
     apply (rule lists.Nil)
-   apply (rule IT.Beta [where ?ss = "[]", unfold foldl_Nil [THEN eq_reflection]])
+   apply (rule IT.Beta [where ?ss = "[]", unfolded foldl_Nil [THEN eq_reflection]])
     apply (erule subst_Var_IT)
    apply (rule Var_IT)
   apply (subst app_last)
@@ -347,7 +347,7 @@
 
 subsection {* Well-typed substitution preserves termination *}
 
-lemma subst_type_IT [rulify]:
+lemma subst_type_IT [rulified]:
   "\<forall>t. t \<in> IT --> (\<forall>e T u i.
     (\<lambda>j. if j < i then e j
           else if j = i then U
@@ -454,7 +454,7 @@
    apply simp
   apply (rule subst_type_IT)
   apply (rule lists.Nil
-    [THEN 2 lists.Cons [THEN IT.Var], unfold foldl_Nil [THEN eq_reflection]
+    [THEN 2 lists.Cons [THEN IT.Var], unfolded foldl_Nil [THEN eq_reflection]
       foldl_Cons [THEN eq_reflection]])
       apply (erule lift_IT)
      apply (rule typing.App)