# HG changeset patch
# User wenzelm
# Date 968353811 -7200
# Node ID 5c027cca6262e6121c89260d3a0e8d4dccb72bc8
# Parent  14a71104a4980384608c28c327d984be6ddc626b
updated attribute names;

diff -r 14a71104a498 -r 5c027cca6262 src/HOL/Induct/Acc.thy
--- a/src/HOL/Induct/Acc.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Induct/Acc.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -18,7 +18,7 @@
 
 inductive "acc r"
   intros
-    accI [rulify_prems]:
+    accI [rulified]:
       "\<forall>y. (y, x) \<in> r --> y \<in> acc r ==> x \<in> acc r"
 
 syntax
diff -r 14a71104a498 -r 5c027cca6262 src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -154,7 +154,7 @@
 
   have "?B (Suc m) = ?t Un ?B m"; by (simp add: Sigma_Suc);
   also; have "... : ?T";
-  proof (rule tiling_Un [rulify]);
+  proof (rule tiling_Un [rulified]);
     show "?t : ?T"; by (rule dominoes_tile_row);
     from hyp; show "?B m : ?T"; .;
     show "?t Int ?B m = {}"; by blast;
diff -r 14a71104a498 -r 5c027cca6262 src/HOL/Isar_examples/Puzzle.thy
--- a/src/HOL/Isar_examples/Puzzle.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Isar_examples/Puzzle.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -118,7 +118,7 @@
     proof;
       assume "n < f n";
       hence "Suc n <= f n"; by (rule Suc_leI);
-      hence "f (Suc n) <= f (f n)"; by (rule mono [rulify]);
+      hence "f (Suc n) <= f (f n)"; by (rule mono [rulified]);
       also; have "... < f (Suc n)"; by (rule f_ax);
       finally; have "... < ..."; .; thus False; ..;
     qed;
diff -r 14a71104a498 -r 5c027cca6262 src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Lambda/Eta.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -45,7 +45,7 @@
 
 subsection "Properties of eta, subst and free"
 
-lemma subst_not_free [rulify, simp]:
+lemma subst_not_free [rulified, simp]:
     "\<forall>i t u. \<not> free s i --> s[t/i] = s[u/i]"
   apply (induct_tac s)
     apply (simp_all add: subst_Var)
@@ -74,7 +74,7 @@
   apply simp_all
   done
 
-lemma free_eta [rulify]:
+lemma free_eta [rulified]:
     "s -e> t ==> \<forall>i. free t i = free s i"
   apply (erule eta.induct)
      apply (simp_all cong: conj_cong)
@@ -85,7 +85,7 @@
   apply (simp add: free_eta)
   done
 
-lemma eta_subst [rulify, simp]:
+lemma eta_subst [rulified, simp]:
     "s -e> t ==> \<forall>u i. s[u/i] -e> t[u/i]"
   apply (erule eta.induct)
   apply (simp_all add: subst_subst [symmetric])
@@ -136,13 +136,13 @@
 
 subsection "Commutation of beta and eta"
 
-lemma free_beta [rulify]:
+lemma free_beta [rulified]:
     "s -> t ==> \<forall>i. free t i --> free s i"
   apply (erule beta.induct)
      apply simp_all
   done
 
-lemma beta_subst [rulify, intro]:
+lemma beta_subst [rulified, intro]:
     "s -> t ==> \<forall>u i. s[u/i] -> t[u/i]"
   apply (erule beta.induct)
      apply (simp_all add: subst_subst [symmetric])
@@ -153,13 +153,13 @@
   apply (auto elim!: linorder_neqE simp: subst_Var)
   done
 
-lemma eta_lift [rulify, simp]:
+lemma eta_lift [rulified, simp]:
     "s -e> t ==> \<forall>i. lift s i -e> lift t i"
   apply (erule eta.induct)
      apply simp_all
   done
 
-lemma rtrancl_eta_subst [rulify]:
+lemma rtrancl_eta_subst [rulified]:
     "\<forall>s t i. s -e> t --> u[s/i] -e>> u[t/i]"
   apply (induct_tac u)
     apply (simp_all add: subst_Var)
@@ -190,7 +190,7 @@
 
 text {* @{term "Abs (lift s 0 $ Var 0) -e> s"} *}
 
-lemma not_free_iff_lifted [rulify]:
+lemma not_free_iff_lifted [rulified]:
     "\<forall>i. (\<not> free s i) = (\<exists>t. s = lift t i)"
   apply (induct_tac s)
     apply simp
diff -r 14a71104a498 -r 5c027cca6262 src/HOL/Lambda/InductTermi.thy
--- a/src/HOL/Lambda/InductTermi.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Lambda/InductTermi.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -26,7 +26,7 @@
 
 subsection {* Every term in IT terminates *}
 
-lemma double_induction_lemma [rulify]:
+lemma double_induction_lemma [rulified]:
   "s : termi beta ==> \<forall>t. t : termi beta -->
     (\<forall>r ss. t = r[s/0] $$ ss --> Abs r $ s $$ ss : termi beta)"
   apply (erule acc_induct)
diff -r 14a71104a498 -r 5c027cca6262 src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Lambda/Lambda.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -120,7 +120,7 @@
   apply (simp add: subst_Var)
   done
 
-lemma lift_lift [rulify]:
+lemma lift_lift [rulified]:
     "\<forall>i k. i < k + 1 --> lift (lift t i) (Suc k) = lift (lift t k) i"
   apply (induct_tac t)
     apply auto
@@ -144,7 +144,7 @@
     apply simp_all
   done
 
-lemma subst_subst [rulify]:
+lemma subst_subst [rulified]:
     "\<forall>i j u v. i < j + 1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
   apply (induct_tac t)
     apply (simp_all
@@ -183,19 +183,19 @@
 text {* Not used in Church-Rosser proof, but in Strong
   Normalization. \medskip *}
 
-theorem subst_preserves_beta [rulify, simp]:
+theorem subst_preserves_beta [rulified, simp]:
     "r -> s ==> \<forall>t i. r[t/i] -> s[t/i]"
   apply (erule beta.induct)
      apply (simp_all add: subst_subst [symmetric])
   done
 
-theorem lift_preserves_beta [rulify, simp]:
+theorem lift_preserves_beta [rulified, simp]:
     "r -> s ==> \<forall>i. lift r i -> lift s i"
   apply (erule beta.induct)
      apply auto
   done
 
-theorem subst_preserves_beta2 [rulify, simp]:
+theorem subst_preserves_beta2 [rulified, simp]:
     "\<forall>r s i. r -> s --> t[r/i] ->> t[s/i]"
   apply (induct_tac t)
     apply (simp add: subst_Var r_into_rtrancl)
diff -r 14a71104a498 -r 5c027cca6262 src/HOL/Lambda/ListApplication.thy
--- a/src/HOL/Lambda/ListApplication.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Lambda/ListApplication.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -18,13 +18,13 @@
    apply auto
   done
 
-lemma Var_eq_apps_conv [rulify, iff]:
+lemma Var_eq_apps_conv [rulified, iff]:
     "\<forall>s. (Var m = s $$ ss) = (Var m = s \<and> ss = [])"
   apply (induct_tac ss)
    apply auto
   done
 
-lemma Var_apps_eq_Var_apps_conv [rulify, iff]:
+lemma Var_apps_eq_Var_apps_conv [rulified, iff]:
     "\<forall>ss. (Var m $$ rs = Var n $$ ss) = (m = n \<and> rs = ss)"
   apply (induct_tac rs rule: rev_induct)
    apply simp
@@ -69,7 +69,7 @@
    apply auto
   done
 
-lemma Var_apps_neq_Abs_apps [rulify, iff]:
+lemma Var_apps_neq_Abs_apps [rulified, iff]:
     "\<forall>ts. Var n $$ ts ~= Abs r $$ ss"
   apply (induct_tac ss rule: rev_induct)
    apply simp
@@ -103,7 +103,7 @@
 
 text {* \medskip A customized induction schema for @{text "$$"}. *}
 
-lemma lem [rulify]:
+lemma lem [rulified (no_asm)]:
   "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
     !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
   |] ==> \<forall>t. size t = n --> P t"
diff -r 14a71104a498 -r 5c027cca6262 src/HOL/Lambda/ListBeta.thy
--- a/src/HOL/Lambda/ListBeta.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Lambda/ListBeta.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -96,7 +96,7 @@
   apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
   done
 
-lemma apps_preserves_betas [rulify, simp]:
+lemma apps_preserves_betas [rulified, simp]:
     "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss"
   apply (induct_tac rs rule: rev_induct)
    apply simp
diff -r 14a71104a498 -r 5c027cca6262 src/HOL/Lambda/ListOrder.thy
--- a/src/HOL/Lambda/ListOrder.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Lambda/ListOrder.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -64,7 +64,7 @@
   apply (blast intro: append_eq_appendI)
   done
 
-lemma Cons_step1E [rulify_prems, elim!]:
+lemma Cons_step1E [rulified, elim!]:
   "[| (ys, x # xs) \<in> step1 r;
     \<forall>y. ys = y # xs --> (y, x) \<in> r --> R;
     \<forall>zs. ys = x # zs --> (zs, xs) \<in> step1 r --> R
@@ -87,7 +87,7 @@
   apply blast
   done
 
-lemma Cons_acc_step1I [rulify, intro!]:
+lemma Cons_acc_step1I [rulified, intro!]:
     "x \<in> acc r ==> \<forall>xs. xs \<in> acc (step1 r) --> x # xs \<in> acc (step1 r)"
   apply (erule acc_induct)
   apply (erule thin_rl)
diff -r 14a71104a498 -r 5c027cca6262 src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Lambda/ParRed.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -70,13 +70,13 @@
 
 subsection {* Misc properties of par-beta *}
 
-lemma par_beta_lift [rulify, simp]:
+lemma par_beta_lift [rulified, simp]:
     "\<forall>t' n. t => t' --> lift t n => lift t' n"
   apply (induct_tac t)
     apply fastsimp+
   done
 
-lemma par_beta_subst [rulify]:
+lemma par_beta_subst [rulified]:
     "\<forall>s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]"
   apply (induct_tac t)
     apply (simp add: subst_Var)
@@ -110,7 +110,7 @@
   "cd (Abs u $ t) = (cd u)[cd t/0]"
   "cd (Abs s) = Abs (cd s)"
 
-lemma par_beta_cd [rulify]:
+lemma par_beta_cd [rulified]:
     "\<forall>t. s => t --> t => cd s"
   apply (induct_tac s rule: cd.induct)
       apply auto
diff -r 14a71104a498 -r 5c027cca6262 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)
diff -r 14a71104a498 -r 5c027cca6262 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -587,7 +587,7 @@
 by (auto simp add: correct_state_def Let_def)
 
 
-lemma BV_correct_1 [rulify]:
+lemma BV_correct_1 [rulified]:
 "\<And>state. \<lbrakk> wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>\<rbrakk> 
  \<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (simp only: split_tupled_all)
@@ -617,7 +617,7 @@
 done
 
 
-theorem BV_correct [rulify]:
+theorem BV_correct [rulified]:
 "\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s -jvm\<rightarrow> t \<rbrakk> \<Longrightarrow> G,phi \<turnstile>JVM s\<surd> \<longrightarrow> G,phi \<turnstile>JVM t\<surd>"
 apply (unfold exec_all_def)
 apply (erule rtrancl_induct)
diff -r 14a71104a498 -r 5c027cca6262 src/HOL/MicroJava/BV/Convert.thy
--- a/src/HOL/MicroJava/BV/Convert.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/MicroJava/BV/Convert.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -383,7 +383,7 @@
 qed
 
 
-theorem sup_loc_update [rulify]:
+theorem sup_loc_update [rulified]:
   "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow> 
           (G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x")
 proof (induct x)
@@ -485,7 +485,7 @@
 
   with G
   show ?thesis 
-    by (auto intro!: all_nth_sup_loc [rulify] dest!: sup_loc_length) 
+    by (auto intro!: all_nth_sup_loc [rulified] dest!: sup_loc_length) 
 qed
   
 
diff -r 14a71104a498 -r 5c027cca6262 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -92,11 +92,11 @@
   "approx_val G hp Null (Ok (RefT x))"
 by (auto intro: null simp add: approx_val_def)
 
-lemma approx_val_imp_approx_val_assConvertible [rulify]: 
+lemma approx_val_imp_approx_val_assConvertible [rulified]: 
   "wf_prog wt G \<Longrightarrow> approx_val G hp v (Ok T) \<longrightarrow> G\<turnstile> T\<preceq>T' \<longrightarrow> approx_val G hp v (Ok T')"
 by (cases T) (auto intro: conf_widen simp add: approx_val_def)
 
-lemma approx_val_imp_approx_val_sup_heap [rulify]:
+lemma approx_val_imp_approx_val_sup_heap [rulified]:
   "approx_val G hp v at \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_val G hp' v at"
 apply (simp add: approx_val_def split: err.split)
 apply (blast intro: conf_hext)
@@ -107,7 +107,7 @@
   \<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v\<Colon>\<preceq>T"
 by (cases v, auto simp add: obj_ty_def conf_def)
 
-lemma approx_val_imp_approx_val_sup [rulify]:
+lemma approx_val_imp_approx_val_sup [rulified]:
   "wf_prog wt G \<Longrightarrow> (approx_val G h v us) \<longrightarrow> (G \<turnstile> us <=o us') \<longrightarrow> (approx_val G h v us')"
 apply (simp add: sup_PTS_eq approx_val_def split: err.split)
 apply (blast intro: conf_widen)
@@ -128,7 +128,7 @@
   "approx_loc G hp (s#xs) (l#ls) = (approx_val G hp s l \<and> approx_loc G hp xs ls)"
 by (simp add: approx_loc_def)
 
-lemma assConv_approx_stk_imp_approx_loc [rulify]:
+lemma assConv_approx_stk_imp_approx_loc [rulified]:
   "wf_prog wt G \<Longrightarrow> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G) 
   \<longrightarrow> length tys_n = length ts \<longrightarrow> approx_stk G hp s tys_n \<longrightarrow> 
   approx_loc G hp s (map Ok ts)"
@@ -139,7 +139,7 @@
 .
 
 
-lemma approx_loc_imp_approx_loc_sup_heap [rulify]:
+lemma approx_loc_imp_approx_loc_sup_heap [rulified]:
   "\<forall>lvars. approx_loc G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_loc G hp' lvars lt"
 apply (unfold approx_loc_def list_all2_def)
 apply (cases lt)
@@ -149,7 +149,7 @@
 apply auto
 .
 
-lemma approx_loc_imp_approx_loc_sup [rulify]:
+lemma approx_loc_imp_approx_loc_sup [rulified]:
   "wf_prog wt G \<Longrightarrow> approx_loc G hp lvars lt \<longrightarrow> G \<turnstile> lt <=l lt' \<longrightarrow> approx_loc G hp lvars lt'"
 apply (unfold sup_loc_def approx_loc_def list_all2_def)
 apply (auto simp add: all_set_conv_all_nth)
@@ -157,7 +157,7 @@
 .
 
 
-lemma approx_loc_imp_approx_loc_subst [rulify]:
+lemma approx_loc_imp_approx_loc_subst [rulified]:
   "\<forall>loc idx x X. (approx_loc G hp loc LT) \<longrightarrow> (approx_val G hp x X) 
   \<longrightarrow> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))"
 apply (unfold approx_loc_def list_all2_def)
@@ -167,7 +167,7 @@
 
 lemmas [cong] = conj_cong 
 
-lemma approx_loc_append [rulify]:
+lemma approx_loc_append [rulified]:
   "\<forall>L1 l2 L2. length l1=length L1 \<longrightarrow> 
   approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
 apply (unfold approx_loc_def list_all2_def)
@@ -191,11 +191,11 @@
 by (auto intro: subst [OF approx_stk_rev_lem])
 
 
-lemma approx_stk_imp_approx_stk_sup_heap [rulify]:
+lemma approx_stk_imp_approx_stk_sup_heap [rulified]:
   "\<forall>lvars. approx_stk G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_stk G hp' lvars lt"
 by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def)
 
-lemma approx_stk_imp_approx_stk_sup [rulify]:
+lemma approx_stk_imp_approx_stk_sup [rulified]:
   "wf_prog wt G \<Longrightarrow> approx_stk G hp lvars st \<longrightarrow> (G \<turnstile> map Ok st <=l (map Ok st')) 
   \<longrightarrow> approx_stk G hp lvars st'" 
 by (auto intro: approx_loc_imp_approx_loc_sup simp add: approx_stk_def)
@@ -232,13 +232,13 @@
 .
 
 
-lemma oconf_imp_oconf_field_update [rulify]:
+lemma oconf_imp_oconf_field_update [rulified]:
   "\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v\<Colon>\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
   \<Longrightarrow> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
 by (simp add: oconf_def lconf_def)
 
 
-lemma oconf_imp_oconf_heap_newref [rulify]:
+lemma oconf_imp_oconf_heap_newref [rulified]:
 "hp x = None \<longrightarrow> G,hp\<turnstile>obj\<surd> \<longrightarrow> G,hp\<turnstile>obj'\<surd> \<longrightarrow> G,(hp(newref hp\<mapsto>obj'))\<turnstile>obj\<surd>"
 apply (unfold oconf_def lconf_def)
 apply simp
@@ -246,7 +246,7 @@
 .
 
 
-lemma oconf_imp_oconf_heap_update [rulify]:
+lemma oconf_imp_oconf_heap_update [rulified]:
   "hp a = Some obj' \<longrightarrow> obj_ty obj' = obj_ty obj'' \<longrightarrow> G,hp\<turnstile>obj\<surd> 
   \<longrightarrow> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
 apply (unfold oconf_def lconf_def)
@@ -258,13 +258,13 @@
 (** hconf **)
 
 
-lemma hconf_imp_hconf_newref [rulify]:
+lemma hconf_imp_hconf_newref [rulified]:
   "hp x = None \<longrightarrow> G\<turnstile>h hp\<surd> \<longrightarrow> G,hp\<turnstile>obj\<surd> \<longrightarrow> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>"
 apply (simp add: hconf_def)
 apply (fast intro: oconf_imp_oconf_heap_newref)
 .
 
-lemma hconf_imp_hconf_field_update [rulify]:
+lemma hconf_imp_hconf_field_update [rulified]:
   "map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and> 
   G,hp\<turnstile>v\<Colon>\<preceq>T \<and> G\<turnstile>h hp\<surd> \<longrightarrow> G\<turnstile>h hp(oloc \<mapsto> (oT, fs((F,D)\<mapsto>v)))\<surd>"
 apply (simp add: hconf_def)
@@ -276,7 +276,7 @@
 
 lemmas [simp del] = fun_upd_apply
 
-lemma correct_frames_imp_correct_frames_field_update [rulify]:
+lemma correct_frames_imp_correct_frames_field_update [rulified]:
   "\<forall>rT C sig. correct_frames G hp phi rT sig frs \<longrightarrow> 
   hp a = Some (C,od) \<longrightarrow> map_of (fields (G, C)) fl = Some fd \<longrightarrow> 
   G,hp\<turnstile>v\<Colon>\<preceq>fd 
@@ -299,7 +299,7 @@
 apply simp
 .
 
-lemma correct_frames_imp_correct_frames_newref [rulify]:
+lemma correct_frames_imp_correct_frames_newref [rulified]:
   "\<forall>rT C sig. hp x = None \<longrightarrow> correct_frames G hp phi rT sig frs \<and> oconf G hp obj 
   \<longrightarrow> correct_frames G (hp(newref hp \<mapsto> obj)) phi rT sig frs"
 apply (induct frs)
diff -r 14a71104a498 -r 5c027cca6262 src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -161,7 +161,7 @@
     case None
     with wtl fits
     show ?thesis 
-      by - (rule wtl_inst_mono [elimify], (simp add: wtl_cert_def)+)
+      by - (rule wtl_inst_mono [elimified], (simp add: wtl_cert_def)+)
   next
     case Some
     with wtl fits
@@ -406,7 +406,7 @@
   "[| wt_method G C pTs rT mxl ins phi; fits ins cert phi |] ==> 
   wtl_method G C pTs rT mxl ins cert"
 by (simp add: wt_method_def wtl_method_def)
-   (rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def) 
+   (rule wt_imp_wtl_inst_list [rulified, elimified], auto simp add: wt_start_def) 
 
 
 lemma wtl_method_complete:
@@ -462,17 +462,17 @@
 
     from 1
     show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))"
-    proof (rule bspec [elimify], clarsimp)
+    proof (rule bspec [elimified], clarsimp)
       assume ub : "unique b"
       assume m: "\<forall>(sig,rT,mb)\<in>set b. wf_mhead G sig rT \<and> 
                   (\<lambda>(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb" 
       from m b
       show ?thesis
-      proof (rule bspec [elimify], clarsimp)
+      proof (rule bspec [elimified], clarsimp)
         assume "wt_method G a ba ad ae bb (Phi a (ac, ba))"         
         with wfprog uG ub b 1
         show ?thesis
-          by - (rule wtl_method_complete [elimify], assumption+, 
+          by - (rule wtl_method_complete [elimified], assumption+, 
                 simp add: make_Cert_def unique_epsilon)
       qed 
     qed
diff -r 14a71104a498 -r 5c027cca6262 src/HOL/MicroJava/BV/LBVCorrect.thy
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -264,7 +264,7 @@
   assume wtl: "wtl_inst_list ins G rT cert (length ins) 0 ?s0 \<noteq> Err"
 
   obtain phi where fits: "fits phi ins G rT ?s0 cert"    
-    by (rule exists_phi [elimify]) blast
+    by (rule exists_phi [elimified]) blast
 
   with wtl
   have allpc:
diff -r 14a71104a498 -r 5c027cca6262 src/HOL/MicroJava/BV/StepMono.thy
--- a/src/HOL/MicroJava/BV/StepMono.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/MicroJava/BV/StepMono.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -13,7 +13,7 @@
   by (auto elim: widen.elims)
 
 
-lemma sup_loc_some [rulify]:
+lemma sup_loc_some [rulified]:
 "\<forall> y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = Ok t \<longrightarrow> 
   (\<exists>t. b!n = Ok t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
 proof (induct (open) ?P b)
@@ -59,7 +59,7 @@
 qed
  
 
-lemma append_length_n [rulify]: 
+lemma append_length_n [rulified]: 
 "\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
 proof (induct (open) ?P x)
   show "?P []" by simp
@@ -78,7 +78,7 @@
       fix "n'" assume s: "n = Suc n'"
       with l 
       have  "n' \<le> length ls" by simp 
-      hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rulify])
+      hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rulified])
       thus ?thesis
       proof elim
         fix a b 
@@ -254,7 +254,7 @@
         have "length list < length (fst s2)" 
           by (simp add: sup_state_length)
         hence "\<exists>a b c. (fst s2) = rev a @ b # c \<and> length a = length list"
-          by (rule rev_append_cons [rulify])
+          by (rule rev_append_cons [rulified])
         thus ?thesis
           by -  (cases s2, elim exE conjE, simp, rule that) 
       qed
diff -r 14a71104a498 -r 5c027cca6262 src/HOL/Real/HahnBanach/Aux.thy
--- a/src/HOL/Real/HahnBanach/Aux.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -12,7 +12,7 @@
 
 lemmas [intro?] = isLub_isUb
 lemmas [intro?] = chainD 
-lemmas chainE2 = chainD2 [elimify]
+lemmas chainE2 = chainD2 [elimified]
 
 text_raw {* \medskip *}
 text{* Lemmas about sets. *}
diff -r 14a71104a498 -r 5c027cca6262 src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -273,7 +273,7 @@
     by case analysis on $a$. *};
 
     also; have "... <= p (y + a \<cdot> x0)";
-    proof (rule linorder_less_split); 
+    proof (rule linorder_cases);
 
       assume z: "a = #0"; 
       with vs y a; show ?thesis; by simp;
diff -r 14a71104a498 -r 5c027cca6262 src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -227,7 +227,7 @@
   "x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)"
     by (unfold vs_sum_def) fast
 
-lemmas vs_sumE = vs_sumD [THEN iffD1, elimify, standard]
+lemmas vs_sumE = vs_sumD [THEN iffD1, elimified, standard]
 
 lemma vs_sumI [intro?]: 
   "[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V"
diff -r 14a71104a498 -r 5c027cca6262 src/HOL/ex/Primes.thy
--- a/src/HOL/ex/Primes.thy	Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/ex/Primes.thy	Thu Sep 07 21:10:11 2000 +0200
@@ -71,7 +71,7 @@
 
 (*Maximality: for all m,n,f naturals, 
                 if f divides m and f divides n then f divides gcd(m,n)*)
-lemma gcd_greatest [rulify]: "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)"
+lemma gcd_greatest [rulified]: "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)"
   apply (induct_tac m n rule: gcd_induct)
   apply (simp_all add: gcd_non_0 dvd_mod);
   done;