# HG changeset patch
# User wenzelm
# Date 968789603 -7200
# Node ID fe05af7ec8162c0584838c9a0e3c29b81b475b1f
# Parent  102f2430cef9440c2d9fda897a19d20836414904
renamed atts: rulify to rule_format, elimify to elim_format;

diff -r 102f2430cef9 -r fe05af7ec816 NEWS
--- a/NEWS	Tue Sep 12 19:03:13 2000 +0200
+++ b/NEWS	Tue Sep 12 22:13:23 2000 +0200
@@ -52,8 +52,8 @@
 
 * ZF: new treatment of arithmetic (nat & int) may break some old proofs;
 
-* Isar/Provers: intro/elim/dest attributes: changed
-intro/intro!/intro!!  flags to intro!/intro/intro? (in most cases, one
+* Isar/Provers: intro/elim/dest attributes changed; renamed
+intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one
 should have to change intro!! to intro? only); replaced "delrule" by
 "rule del";
 
@@ -61,7 +61,7 @@
 
 * Isar: renamed 'RS' attribute to 'THEN';
 
-* Isar: renamed some attributes (rulify -> rulified, elimify -> elimified, ...);
+* Isar: renamed some attributes (rulify -> rule_format, elimify -> elim_format, ...);
 
 * Isar/HOL: renamed "intrs" to "intros" in inductive definitions;
 
@@ -192,9 +192,10 @@
 'inductive_cases' command and 'ind_cases' method; NOTE: use (cases
 (simplified)) method in proper proofs;
 
-* Provers: intro/elim/dest attributes: changed intro/intro!/intro!!
-flags to intro!/intro/intro? (in most cases, one should have to change
-intro!! to intro? only); replaced "delrule" by "rule del";
+* Provers: intro/elim/dest attributes changed; renamed
+intro/intro!/intro!! flags to intro!/intro/intro? (INCOMPATIBILITY, in
+most cases, one should have to change intro!! to intro? only);
+replaced "delrule" by "rule del";
 
 * names of theorems etc. may be natural numbers as well;
 
@@ -336,6 +337,9 @@
 
 *** General ***
 
+* Provers: delrules now handles destruct rules as well (no longer need
+explicit make_elim);
+
 * Provers: blast(_tac) now handles actual object-logic rules as
 assumptions; note that auto(_tac) uses blast(_tac) internally as well;
 
diff -r 102f2430cef9 -r fe05af7ec816 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Tue Sep 12 19:03:13 2000 +0200
+++ b/doc-src/IsarRef/generic.tex	Tue Sep 12 22:13:23 2000 +0200
@@ -305,7 +305,7 @@
 
 
 \indexisaratt{standard}
-\indexisaratt{elimified}
+\indexisaratt{elim-format}
 \indexisaratt{no-vars}
 
 \indexisaratt{THEN}\indexisaratt{COMP}
@@ -320,7 +320,7 @@
   unfolded & : & \isaratt \\
   folded & : & \isaratt \\[0.5ex]
   standard & : & \isaratt \\
-  elimified & : & \isaratt \\
+  elim_format & : & \isaratt \\
   no_vars^* & : & \isaratt \\
   exported^* & : & \isaratt \\
 \end{matharray}
@@ -356,8 +356,8 @@
   given meta-level definitions throughout a rule.
 \item [$standard$] puts a theorem into the standard form of object-rules, just
   as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
-\item [$elimified$] turns an destruction rule into an elimination, just as the
-  ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
+\item [$elim_format$] turns a destruction rule into elimination rule format;
+  see also the ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
 \item [$no_vars$] replaces schematic variables by free ones; this is mainly
   for tuning output of pretty printed theorems.
 \item [$exported$] lifts a local result out of the current proof context,
diff -r 102f2430cef9 -r fe05af7ec816 doc-src/IsarRef/hol.tex
--- a/doc-src/IsarRef/hol.tex	Tue Sep 12 19:03:13 2000 +0200
+++ b/doc-src/IsarRef/hol.tex	Tue Sep 12 22:13:23 2000 +0200
@@ -3,21 +3,24 @@
 
 \section{Miscellaneous attributes}
 
-\indexisaratt{rulified}
+\indexisaratt{rule-format}
 \begin{matharray}{rcl}
-  rulified & : & \isaratt \\
+  rule_format & : & \isaratt \\
 \end{matharray}
 
+\railalias{ruleformat}{rule\_format}
+\railterm{ruleformat}
+
 \begin{rail}
-  'rulified' ('(' noasm ')')?
+  ruleformat ('(' noasm ')')?
   ;
 \end{rail}
 
 \begin{descr}
   
-\item [$rulified$] causes a theorem to be put into standard object-rule form,
-  replacing implication and (bounded) universal quantification of HOL by the
-  corresponding meta-logical connectives.  By default, the result is fully
+\item [$rule_format$] causes a theorem to be put into standard object-rule
+  form, replacing implication and (bounded) universal quantification of HOL by
+  the corresponding meta-logical connectives.  By default, the result is fully
   normalized, including assumptions and conclusions at any depth.  The
   $no_asm$ option restricts the transformation to the conclusion of a rule.
 \end{descr}
diff -r 102f2430cef9 -r fe05af7ec816 doc-src/IsarRef/refcard.tex
--- a/doc-src/IsarRef/refcard.tex	Tue Sep 12 19:03:13 2000 +0200
+++ b/doc-src/IsarRef/refcard.tex	Tue Sep 12 22:13:23 2000 +0200
@@ -118,8 +118,8 @@
   $of~\vec t$ & rule applied to terms (skipping ``$_$'') \\
   $symmetric$ & resolution with symmetry of equality \\
   $THEN~b$ & resolution with other rule \\
-  $rulified$ & result put into standard rule form \\
-  $elimified$ & destruct rule turned into elimination rule \\
+  $rule_format$ & result put into standard rule format \\
+  $elim_format$ & destruct rule turned into elimination rule format \\
   $standard$ & result put into standard form \\[1ex]
 
   \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex]
diff -r 102f2430cef9 -r fe05af7ec816 doc-src/TutorialI/Misc/AdvancedInd.thy
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Sep 12 22:13:23 2000 +0200
@@ -94,10 +94,10 @@
 
 text{*\noindent
 or the wholesale stripping of @{text"\<forall>"} and
-@{text"\<longrightarrow>"} in the conclusion via @{text"rulified"} 
+@{text"\<longrightarrow>"} in the conclusion via @{text"rule_format"} 
 *};
 
-lemmas myrule = simple[rulified];
+lemmas myrule = simple[rule_format];
 
 text{*\noindent
 yielding @{thm"myrule"[no_vars]}.
@@ -105,7 +105,7 @@
 statement of your original lemma, thus avoiding the intermediate step:
 *};
 
-lemma myrule[rulified]:  "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
+lemma myrule[rule_format]:  "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
 (*<*)
 by blast;
 (*>*)
@@ -206,14 +206,14 @@
 We can now derive the desired @{prop"i <= f i"} from @{text"f_incr"}:
 *};
 
-lemmas f_incr = f_incr_lem[rulified, OF refl];
+lemmas f_incr = f_incr_lem[rule_format, OF refl];
 
 text{*\noindent
 The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}. Again,
 we could have included this derivation in the original statement of the lemma:
 *};
 
-lemma f_incr[rulified, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
+lemma f_incr[rule_format, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
 (*<*)oops;(*>*)
 
 text{*
diff -r 102f2430cef9 -r fe05af7ec816 src/HOL/Induct/Acc.thy
--- a/src/HOL/Induct/Acc.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Induct/Acc.thy	Tue Sep 12 22:13:23 2000 +0200
@@ -18,7 +18,7 @@
 
 inductive "acc r"
   intros
-    accI [rulified]:
+    accI [rule_format]:
       "\<forall>y. (y, x) \<in> r --> y \<in> acc r ==> x \<in> acc r"
 
 syntax
diff -r 102f2430cef9 -r fe05af7ec816 src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Tue Sep 12 22:13:23 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 [rulified]);
+  proof (rule tiling_Un [rule_format]);
     show "?t : ?T"; by (rule dominoes_tile_row);
     from hyp; show "?B m : ?T"; .;
     show "?t Int ?B m = {}"; by blast;
diff -r 102f2430cef9 -r fe05af7ec816 src/HOL/Isar_examples/Puzzle.thy
--- a/src/HOL/Isar_examples/Puzzle.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Isar_examples/Puzzle.thy	Tue Sep 12 22:13:23 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 [rulified]);
+      hence "f (Suc n) <= f (f n)"; by (rule mono [rule_format]);
       also; have "... < f (Suc n)"; by (rule f_ax);
       finally; have "... < ..."; .; thus False; ..;
     qed;
diff -r 102f2430cef9 -r fe05af7ec816 src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Lambda/Eta.thy	Tue Sep 12 22:13:23 2000 +0200
@@ -45,7 +45,7 @@
 
 subsection "Properties of eta, subst and free"
 
-lemma subst_not_free [rulified, simp]:
+lemma subst_not_free [rule_format, 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 [rulified]:
+lemma free_eta [rule_format]:
     "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 [rulified, simp]:
+lemma eta_subst [rule_format, 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 [rulified]:
+lemma free_beta [rule_format]:
     "s -> t ==> \<forall>i. free t i --> free s i"
   apply (erule beta.induct)
      apply simp_all
   done
 
-lemma beta_subst [rulified, intro]:
+lemma beta_subst [rule_format, 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 [rulified, simp]:
+lemma eta_lift [rule_format, 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 [rulified]:
+lemma rtrancl_eta_subst [rule_format]:
     "\<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 [rulified]:
+lemma not_free_iff_lifted [rule_format]:
     "\<forall>i. (\<not> free s i) = (\<exists>t. s = lift t i)"
   apply (induct_tac s)
     apply simp
diff -r 102f2430cef9 -r fe05af7ec816 src/HOL/Lambda/InductTermi.thy
--- a/src/HOL/Lambda/InductTermi.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Lambda/InductTermi.thy	Tue Sep 12 22:13:23 2000 +0200
@@ -26,7 +26,7 @@
 
 subsection {* Every term in IT terminates *}
 
-lemma double_induction_lemma [rulified]:
+lemma double_induction_lemma [rule_format]:
   "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 102f2430cef9 -r fe05af7ec816 src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Lambda/Lambda.thy	Tue Sep 12 22:13:23 2000 +0200
@@ -120,7 +120,7 @@
   apply (simp add: subst_Var)
   done
 
-lemma lift_lift [rulified]:
+lemma lift_lift [rule_format]:
     "\<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 [rulified]:
+lemma subst_subst [rule_format]:
     "\<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 [rulified, simp]:
+theorem subst_preserves_beta [rule_format, 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 [rulified, simp]:
+theorem lift_preserves_beta [rule_format, simp]:
     "r -> s ==> \<forall>i. lift r i -> lift s i"
   apply (erule beta.induct)
      apply auto
   done
 
-theorem subst_preserves_beta2 [rulified, simp]:
+theorem subst_preserves_beta2 [rule_format, 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 102f2430cef9 -r fe05af7ec816 src/HOL/Lambda/ListApplication.thy
--- a/src/HOL/Lambda/ListApplication.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Lambda/ListApplication.thy	Tue Sep 12 22:13:23 2000 +0200
@@ -18,13 +18,13 @@
    apply auto
   done
 
-lemma Var_eq_apps_conv [rulified, iff]:
+lemma Var_eq_apps_conv [rule_format, 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 [rulified, iff]:
+lemma Var_apps_eq_Var_apps_conv [rule_format, 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 [rulified, iff]:
+lemma Var_apps_neq_Abs_apps [rule_format, 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 [rulified (no_asm)]:
+lemma lem [rule_format (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 102f2430cef9 -r fe05af7ec816 src/HOL/Lambda/ListBeta.thy
--- a/src/HOL/Lambda/ListBeta.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Lambda/ListBeta.thy	Tue Sep 12 22:13:23 2000 +0200
@@ -96,7 +96,7 @@
   apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
   done
 
-lemma apps_preserves_betas [rulified, simp]:
+lemma apps_preserves_betas [rule_format, simp]:
     "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss"
   apply (induct_tac rs rule: rev_induct)
    apply simp
diff -r 102f2430cef9 -r fe05af7ec816 src/HOL/Lambda/ListOrder.thy
--- a/src/HOL/Lambda/ListOrder.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Lambda/ListOrder.thy	Tue Sep 12 22:13:23 2000 +0200
@@ -64,7 +64,7 @@
   apply (blast intro: append_eq_appendI)
   done
 
-lemma Cons_step1E [rulified, elim!]:
+lemma Cons_step1E [rule_format, 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 [rulified, intro!]:
+lemma Cons_acc_step1I [rule_format, 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 102f2430cef9 -r fe05af7ec816 src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Lambda/ParRed.thy	Tue Sep 12 22:13:23 2000 +0200
@@ -70,13 +70,13 @@
 
 subsection {* Misc properties of par-beta *}
 
-lemma par_beta_lift [rulified, simp]:
+lemma par_beta_lift [rule_format, simp]:
     "\<forall>t' n. t => t' --> lift t n => lift t' n"
   apply (induct_tac t)
     apply fastsimp+
   done
 
-lemma par_beta_subst [rulified]:
+lemma par_beta_subst [rule_format]:
     "\<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 [rulified]:
+lemma par_beta_cd [rule_format]:
     "\<forall>t. s => t --> t => cd s"
   apply (induct_tac s rule: cd.induct)
       apply auto
diff -r 102f2430cef9 -r fe05af7ec816 src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Lambda/Type.thy	Tue Sep 12 22:13:23 2000 +0200
@@ -74,7 +74,7 @@
 
 text {* Iterated function types *}
 
-lemma list_app_typeD [rulified]:
+lemma list_app_typeD [rule_format]:
     "\<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 [rulified]:
+lemma list_app_typeI [rule_format]:
     "\<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 [rulified]:
+lemma lists_types [rule_format]:
     "\<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 [rulified, simp]:
+lemma lift_map [rule_format, 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 [rulified, simp]:
+lemma subst_map [rule_format, 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 [rulified, intro!]:
+lemma lift_IT [rule_format, 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 [rulified]:
+lemma lifts_IT [rule_format]:
     "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' [rulified]:
+lemma lift_type' [rule_format]:
   "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 [rulified]:
+lemma lift_types [rule_format]:
   "\<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 [rulified]:
+lemma subst_lemma [rule_format]:
   "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 [rulified]:
+lemma substs_lemma [rule_format]:
   "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 [rulified]:
+lemma subject_reduction [rule_format]:
     "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 [rulified]: "r \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT"
+lemma subst_Var_IT [rule_format]: "r \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT"
   apply (erule IT.induct)
     txt {* Case @{term Var}: *}
     apply (intro strip)
@@ -347,7 +347,7 @@
 
 subsection {* Well-typed substitution preserves termination *}
 
-lemma subst_type_IT [rulified]:
+lemma subst_type_IT [rule_format]:
   "\<forall>t. t \<in> IT --> (\<forall>e T u i.
     (\<lambda>j. if j < i then e j
           else if j = i then U
diff -r 102f2430cef9 -r fe05af7ec816 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Sep 12 22:13:23 2000 +0200
@@ -587,7 +587,7 @@
 by (auto simp add: correct_state_def Let_def)
 
 
-lemma BV_correct_1 [rulified]:
+lemma BV_correct_1 [rule_format]:
 "\<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 [rulified]:
+theorem BV_correct [rule_format]:
 "\<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 102f2430cef9 -r fe05af7ec816 src/HOL/MicroJava/BV/Convert.thy
--- a/src/HOL/MicroJava/BV/Convert.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/MicroJava/BV/Convert.thy	Tue Sep 12 22:13:23 2000 +0200
@@ -383,7 +383,7 @@
 qed
 
 
-theorem sup_loc_update [rulified]:
+theorem sup_loc_update [rule_format]:
   "\<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 [rulified] dest!: sup_loc_length) 
+    by (auto intro!: all_nth_sup_loc [rule_format] dest!: sup_loc_length) 
 qed
   
 
diff -r 102f2430cef9 -r fe05af7ec816 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy	Tue Sep 12 22:13:23 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 [rulified]: 
+lemma approx_val_imp_approx_val_assConvertible [rule_format]: 
   "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 [rulified]:
+lemma approx_val_imp_approx_val_sup_heap [rule_format]:
   "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 [rulified]:
+lemma approx_val_imp_approx_val_sup [rule_format]:
   "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 [rulified]:
+lemma assConv_approx_stk_imp_approx_loc [rule_format]:
   "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 [rulified]:
+lemma approx_loc_imp_approx_loc_sup_heap [rule_format]:
   "\<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 [rulified]:
+lemma approx_loc_imp_approx_loc_sup [rule_format]:
   "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 [rulified]:
+lemma approx_loc_imp_approx_loc_subst [rule_format]:
   "\<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 [rulified]:
+lemma approx_loc_append [rule_format]:
   "\<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 [rulified]:
+lemma approx_stk_imp_approx_stk_sup_heap [rule_format]:
   "\<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 [rulified]:
+lemma approx_stk_imp_approx_stk_sup [rule_format]:
   "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 [rulified]:
+lemma oconf_imp_oconf_field_update [rule_format]:
   "\<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 [rulified]:
+lemma oconf_imp_oconf_heap_newref [rule_format]:
 "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 [rulified]:
+lemma oconf_imp_oconf_heap_update [rule_format]:
   "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 [rulified]:
+lemma hconf_imp_hconf_newref [rule_format]:
   "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 [rulified]:
+lemma hconf_imp_hconf_field_update [rule_format]:
   "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 [rulified]:
+lemma correct_frames_imp_correct_frames_field_update [rule_format]:
   "\<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 [rulified]:
+lemma correct_frames_imp_correct_frames_newref [rule_format]:
   "\<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 102f2430cef9 -r fe05af7ec816 src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Tue Sep 12 22:13:23 2000 +0200
@@ -161,7 +161,7 @@
     case None
     with wtl fits
     show ?thesis 
-      by - (rule wtl_inst_mono [elimified], (simp add: wtl_cert_def)+)
+      by - (rule wtl_inst_mono [elim_format], (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 [rulified, elimified], auto simp add: wt_start_def) 
+   (rule wt_imp_wtl_inst_list [rule_format, elim_format], 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 [elimified], clarsimp)
+    proof (rule bspec [elim_format], 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 [elimified], clarsimp)
+      proof (rule bspec [elim_format], 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 [elimified], assumption+, 
+          by - (rule wtl_method_complete [elim_format], assumption+, 
                 simp add: make_Cert_def unique_epsilon)
       qed 
     qed
diff -r 102f2430cef9 -r fe05af7ec816 src/HOL/MicroJava/BV/LBVCorrect.thy
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Tue Sep 12 22:13:23 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 [elimified]) blast
+    by (rule exists_phi [elim_format]) blast
 
   with wtl
   have allpc:
diff -r 102f2430cef9 -r fe05af7ec816 src/HOL/MicroJava/BV/StepMono.thy
--- a/src/HOL/MicroJava/BV/StepMono.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/MicroJava/BV/StepMono.thy	Tue Sep 12 22:13:23 2000 +0200
@@ -13,7 +13,7 @@
   by (auto elim: widen.elims)
 
 
-lemma sup_loc_some [rulified]:
+lemma sup_loc_some [rule_format]:
 "\<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 [rulified]: 
+lemma append_length_n [rule_format]: 
 "\<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 [rulified])
+      hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rule_format])
       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 [rulified])
+          by (rule rev_append_cons [rule_format])
         thus ?thesis
           by -  (cases s2, elim exE conjE, simp, rule that) 
       qed
diff -r 102f2430cef9 -r fe05af7ec816 src/HOL/Real/HahnBanach/Aux.thy
--- a/src/HOL/Real/HahnBanach/Aux.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy	Tue Sep 12 22:13:23 2000 +0200
@@ -12,7 +12,7 @@
 
 lemmas [intro?] = isLub_isUb
 lemmas [intro?] = chainD 
-lemmas chainE2 = chainD2 [elimified]
+lemmas chainE2 = chainD2 [elim_format, standard]
 
 text_raw {* \medskip *}
 text{* Lemmas about sets. *}
diff -r 102f2430cef9 -r fe05af7ec816 src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Tue Sep 12 22:13:23 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, elimified, standard]
+lemmas vs_sumE = vs_sumD [THEN iffD1, elim_format, standard]
 
 lemma vs_sumI [intro?]: 
   "[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V"
diff -r 102f2430cef9 -r fe05af7ec816 src/HOL/ex/Primes.thy
--- a/src/HOL/ex/Primes.thy	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/ex/Primes.thy	Tue Sep 12 22:13:23 2000 +0200
@@ -71,7 +71,7 @@
 
 (*Maximality: for all m,n,k naturals, 
                 if k divides m and k divides n then k divides gcd(m,n)*)
-lemma gcd_greatest [rulified]: "(k dvd m) --> (k dvd n) --> k dvd gcd(m,n)"
+lemma gcd_greatest [rule_format]: "(k dvd m) --> (k dvd n) --> k dvd gcd(m,n)"
   apply (induct_tac m n rule: gcd_induct)
   apply (simp_all add: gcd_non_0 dvd_mod);
   done;
diff -r 102f2430cef9 -r fe05af7ec816 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/Provers/classical.ML	Tue Sep 12 22:13:23 2000 +0200
@@ -1046,10 +1046,11 @@
 
 (* setup_attrs *)
 
-fun elimified x = Attrib.no_args (Drule.rule_attribute (K Data.make_elim)) x;
+fun elim_format x = Attrib.no_args (Drule.rule_attribute (K Data.make_elim)) x;
 
 val setup_attrs = Attrib.add_attributes
- [("elimified", (elimified, elimified), "destruct rule turned into elimination rule (classical)"),
+ [("elim_format", (elim_format, elim_format),
+    "destruct rule turned into elimination rule format (classical)"),
   (destN, cla_attr (op addXDs) (op addDs) (op addSDs), "declaration of destruction rule"),
   (elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "declaration of elimination rule"),
   (introN, cla_attr (op addXIs) (op addIs) (op addSIs), "declaration of introduction rule"),
diff -r 102f2430cef9 -r fe05af7ec816 src/Provers/rulify.ML
--- a/src/Provers/rulify.ML	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/Provers/rulify.ML	Tue Sep 12 22:13:23 2000 +0200
@@ -19,8 +19,8 @@
 signature RULIFY =
 sig
   include BASIC_RULIFY
-  val rulified: 'a attribute
-  val rulified_no_asm: 'a attribute
+  val rule_format: 'a attribute
+  val rule_format_no_asm: 'a attribute
   val setup: (theory -> theory) list
 end;
 
@@ -38,11 +38,11 @@
 
 (* attributes *)
 
-fun rulified x = Drule.rule_attribute (fn _ => rulify) x;
-fun rulified_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
+fun rule_format x = Drule.rule_attribute (fn _ => rulify) x;
+fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
 
-fun rulified_att x = Attrib.syntax
-  (Scan.lift (Args.parens (Args.$$$ "no_asm") >> K rulified_no_asm || Scan.succeed rulified)) x;
+fun rule_format_att x = Attrib.syntax
+  (Scan.lift (Args.parens (Args.$$$ "no_asm") >> K rule_format_no_asm || Scan.succeed rule_format)) x;
 
 
 (* qed commands *)
@@ -60,6 +60,6 @@
 
 val setup =
  [Attrib.add_attributes
-  [("rulified", (rulified_att, rulified_att), "result put into standard rule form")]];
+  [("rule_format", (rule_format_att, rule_format_att), "result put into standard rule format")]];
 
 end;
diff -r 102f2430cef9 -r fe05af7ec816 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue Sep 12 22:13:23 2000 +0200
@@ -269,7 +269,7 @@
 (* misc rules *)
 
 fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) x;
-fun elimified x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x;
+fun elim_format x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x;
 fun no_vars x = no_args (Drule.rule_attribute (K (#1 o Drule.freeze_thaw))) x;
 
 fun exported_global x = no_args (Drule.rule_attribute (Proof.export_thm o ProofContext.init)) x;
@@ -292,7 +292,7 @@
   ("unfolded", (unfolded_global, unfolded_local), "unfolded definitions"),
   ("folded", (folded_global, folded_local), "folded definitions"),
   ("standard", (standard, standard), "result put into standard form"),
-  ("elimified", (elimified, elimified), "destruct rule turned into elimination rule"),
+  ("elim_format", (elim_format, elim_format), "destruct rule turned into elimination rule format"),
   ("no_vars", (no_vars, no_vars), "frozen schematic vars"),
   ("case_names", (case_names, case_names), "named rule cases"),
   ("params", (params, params), "named rule parameters"),