renamed atts: rulify to rule_format, elimify to elim_format;
authorwenzelm
Tue Sep 12 22:13:23 2000 +0200 (2000-09-12)
changeset 9941fe05af7ec816
parent 9940 102f2430cef9
child 9942 87f0809a06a9
renamed atts: rulify to rule_format, elimify to elim_format;
NEWS
doc-src/IsarRef/generic.tex
doc-src/IsarRef/hol.tex
doc-src/IsarRef/refcard.tex
doc-src/TutorialI/Misc/AdvancedInd.thy
src/HOL/Induct/Acc.thy
src/HOL/Isar_examples/MutilatedCheckerboard.thy
src/HOL/Isar_examples/Puzzle.thy
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/InductTermi.thy
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/ListApplication.thy
src/HOL/Lambda/ListBeta.thy
src/HOL/Lambda/ListOrder.thy
src/HOL/Lambda/ParRed.thy
src/HOL/Lambda/Type.thy
src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
src/HOL/MicroJava/BV/Convert.thy
src/HOL/MicroJava/BV/Correct.thy
src/HOL/MicroJava/BV/LBVComplete.thy
src/HOL/MicroJava/BV/LBVCorrect.thy
src/HOL/MicroJava/BV/StepMono.thy
src/HOL/Real/HahnBanach/Aux.thy
src/HOL/Real/HahnBanach/Subspace.thy
src/HOL/ex/Primes.thy
src/Provers/classical.ML
src/Provers/rulify.ML
src/Pure/Isar/attrib.ML
     1.1 --- a/NEWS	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/NEWS	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -52,8 +52,8 @@
     1.4  
     1.5  * ZF: new treatment of arithmetic (nat & int) may break some old proofs;
     1.6  
     1.7 -* Isar/Provers: intro/elim/dest attributes: changed
     1.8 -intro/intro!/intro!!  flags to intro!/intro/intro? (in most cases, one
     1.9 +* Isar/Provers: intro/elim/dest attributes changed; renamed
    1.10 +intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one
    1.11  should have to change intro!! to intro? only); replaced "delrule" by
    1.12  "rule del";
    1.13  
    1.14 @@ -61,7 +61,7 @@
    1.15  
    1.16  * Isar: renamed 'RS' attribute to 'THEN';
    1.17  
    1.18 -* Isar: renamed some attributes (rulify -> rulified, elimify -> elimified, ...);
    1.19 +* Isar: renamed some attributes (rulify -> rule_format, elimify -> elim_format, ...);
    1.20  
    1.21  * Isar/HOL: renamed "intrs" to "intros" in inductive definitions;
    1.22  
    1.23 @@ -192,9 +192,10 @@
    1.24  'inductive_cases' command and 'ind_cases' method; NOTE: use (cases
    1.25  (simplified)) method in proper proofs;
    1.26  
    1.27 -* Provers: intro/elim/dest attributes: changed intro/intro!/intro!!
    1.28 -flags to intro!/intro/intro? (in most cases, one should have to change
    1.29 -intro!! to intro? only); replaced "delrule" by "rule del";
    1.30 +* Provers: intro/elim/dest attributes changed; renamed
    1.31 +intro/intro!/intro!! flags to intro!/intro/intro? (INCOMPATIBILITY, in
    1.32 +most cases, one should have to change intro!! to intro? only);
    1.33 +replaced "delrule" by "rule del";
    1.34  
    1.35  * names of theorems etc. may be natural numbers as well;
    1.36  
    1.37 @@ -336,6 +337,9 @@
    1.38  
    1.39  *** General ***
    1.40  
    1.41 +* Provers: delrules now handles destruct rules as well (no longer need
    1.42 +explicit make_elim);
    1.43 +
    1.44  * Provers: blast(_tac) now handles actual object-logic rules as
    1.45  assumptions; note that auto(_tac) uses blast(_tac) internally as well;
    1.46  
     2.1 --- a/doc-src/IsarRef/generic.tex	Tue Sep 12 19:03:13 2000 +0200
     2.2 +++ b/doc-src/IsarRef/generic.tex	Tue Sep 12 22:13:23 2000 +0200
     2.3 @@ -305,7 +305,7 @@
     2.4  
     2.5  
     2.6  \indexisaratt{standard}
     2.7 -\indexisaratt{elimified}
     2.8 +\indexisaratt{elim-format}
     2.9  \indexisaratt{no-vars}
    2.10  
    2.11  \indexisaratt{THEN}\indexisaratt{COMP}
    2.12 @@ -320,7 +320,7 @@
    2.13    unfolded & : & \isaratt \\
    2.14    folded & : & \isaratt \\[0.5ex]
    2.15    standard & : & \isaratt \\
    2.16 -  elimified & : & \isaratt \\
    2.17 +  elim_format & : & \isaratt \\
    2.18    no_vars^* & : & \isaratt \\
    2.19    exported^* & : & \isaratt \\
    2.20  \end{matharray}
    2.21 @@ -356,8 +356,8 @@
    2.22    given meta-level definitions throughout a rule.
    2.23  \item [$standard$] puts a theorem into the standard form of object-rules, just
    2.24    as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
    2.25 -\item [$elimified$] turns an destruction rule into an elimination, just as the
    2.26 -  ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
    2.27 +\item [$elim_format$] turns a destruction rule into elimination rule format;
    2.28 +  see also the ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
    2.29  \item [$no_vars$] replaces schematic variables by free ones; this is mainly
    2.30    for tuning output of pretty printed theorems.
    2.31  \item [$exported$] lifts a local result out of the current proof context,
     3.1 --- a/doc-src/IsarRef/hol.tex	Tue Sep 12 19:03:13 2000 +0200
     3.2 +++ b/doc-src/IsarRef/hol.tex	Tue Sep 12 22:13:23 2000 +0200
     3.3 @@ -3,21 +3,24 @@
     3.4  
     3.5  \section{Miscellaneous attributes}
     3.6  
     3.7 -\indexisaratt{rulified}
     3.8 +\indexisaratt{rule-format}
     3.9  \begin{matharray}{rcl}
    3.10 -  rulified & : & \isaratt \\
    3.11 +  rule_format & : & \isaratt \\
    3.12  \end{matharray}
    3.13  
    3.14 +\railalias{ruleformat}{rule\_format}
    3.15 +\railterm{ruleformat}
    3.16 +
    3.17  \begin{rail}
    3.18 -  'rulified' ('(' noasm ')')?
    3.19 +  ruleformat ('(' noasm ')')?
    3.20    ;
    3.21  \end{rail}
    3.22  
    3.23  \begin{descr}
    3.24    
    3.25 -\item [$rulified$] causes a theorem to be put into standard object-rule form,
    3.26 -  replacing implication and (bounded) universal quantification of HOL by the
    3.27 -  corresponding meta-logical connectives.  By default, the result is fully
    3.28 +\item [$rule_format$] causes a theorem to be put into standard object-rule
    3.29 +  form, replacing implication and (bounded) universal quantification of HOL by
    3.30 +  the corresponding meta-logical connectives.  By default, the result is fully
    3.31    normalized, including assumptions and conclusions at any depth.  The
    3.32    $no_asm$ option restricts the transformation to the conclusion of a rule.
    3.33  \end{descr}
     4.1 --- a/doc-src/IsarRef/refcard.tex	Tue Sep 12 19:03:13 2000 +0200
     4.2 +++ b/doc-src/IsarRef/refcard.tex	Tue Sep 12 22:13:23 2000 +0200
     4.3 @@ -118,8 +118,8 @@
     4.4    $of~\vec t$ & rule applied to terms (skipping ``$_$'') \\
     4.5    $symmetric$ & resolution with symmetry of equality \\
     4.6    $THEN~b$ & resolution with other rule \\
     4.7 -  $rulified$ & result put into standard rule form \\
     4.8 -  $elimified$ & destruct rule turned into elimination rule \\
     4.9 +  $rule_format$ & result put into standard rule format \\
    4.10 +  $elim_format$ & destruct rule turned into elimination rule format \\
    4.11    $standard$ & result put into standard form \\[1ex]
    4.12  
    4.13    \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex]
     5.1 --- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Sep 12 19:03:13 2000 +0200
     5.2 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Sep 12 22:13:23 2000 +0200
     5.3 @@ -94,10 +94,10 @@
     5.4  
     5.5  text{*\noindent
     5.6  or the wholesale stripping of @{text"\<forall>"} and
     5.7 -@{text"\<longrightarrow>"} in the conclusion via @{text"rulified"} 
     5.8 +@{text"\<longrightarrow>"} in the conclusion via @{text"rule_format"} 
     5.9  *};
    5.10  
    5.11 -lemmas myrule = simple[rulified];
    5.12 +lemmas myrule = simple[rule_format];
    5.13  
    5.14  text{*\noindent
    5.15  yielding @{thm"myrule"[no_vars]}.
    5.16 @@ -105,7 +105,7 @@
    5.17  statement of your original lemma, thus avoiding the intermediate step:
    5.18  *};
    5.19  
    5.20 -lemma myrule[rulified]:  "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
    5.21 +lemma myrule[rule_format]:  "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
    5.22  (*<*)
    5.23  by blast;
    5.24  (*>*)
    5.25 @@ -206,14 +206,14 @@
    5.26  We can now derive the desired @{prop"i <= f i"} from @{text"f_incr"}:
    5.27  *};
    5.28  
    5.29 -lemmas f_incr = f_incr_lem[rulified, OF refl];
    5.30 +lemmas f_incr = f_incr_lem[rule_format, OF refl];
    5.31  
    5.32  text{*\noindent
    5.33  The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}. Again,
    5.34  we could have included this derivation in the original statement of the lemma:
    5.35  *};
    5.36  
    5.37 -lemma f_incr[rulified, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
    5.38 +lemma f_incr[rule_format, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
    5.39  (*<*)oops;(*>*)
    5.40  
    5.41  text{*
     6.1 --- a/src/HOL/Induct/Acc.thy	Tue Sep 12 19:03:13 2000 +0200
     6.2 +++ b/src/HOL/Induct/Acc.thy	Tue Sep 12 22:13:23 2000 +0200
     6.3 @@ -18,7 +18,7 @@
     6.4  
     6.5  inductive "acc r"
     6.6    intros
     6.7 -    accI [rulified]:
     6.8 +    accI [rule_format]:
     6.9        "\<forall>y. (y, x) \<in> r --> y \<in> acc r ==> x \<in> acc r"
    6.10  
    6.11  syntax
     7.1 --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Tue Sep 12 19:03:13 2000 +0200
     7.2 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Tue Sep 12 22:13:23 2000 +0200
     7.3 @@ -154,7 +154,7 @@
     7.4  
     7.5    have "?B (Suc m) = ?t Un ?B m"; by (simp add: Sigma_Suc);
     7.6    also; have "... : ?T";
     7.7 -  proof (rule tiling_Un [rulified]);
     7.8 +  proof (rule tiling_Un [rule_format]);
     7.9      show "?t : ?T"; by (rule dominoes_tile_row);
    7.10      from hyp; show "?B m : ?T"; .;
    7.11      show "?t Int ?B m = {}"; by blast;
     8.1 --- a/src/HOL/Isar_examples/Puzzle.thy	Tue Sep 12 19:03:13 2000 +0200
     8.2 +++ b/src/HOL/Isar_examples/Puzzle.thy	Tue Sep 12 22:13:23 2000 +0200
     8.3 @@ -118,7 +118,7 @@
     8.4      proof;
     8.5        assume "n < f n";
     8.6        hence "Suc n <= f n"; by (rule Suc_leI);
     8.7 -      hence "f (Suc n) <= f (f n)"; by (rule mono [rulified]);
     8.8 +      hence "f (Suc n) <= f (f n)"; by (rule mono [rule_format]);
     8.9        also; have "... < f (Suc n)"; by (rule f_ax);
    8.10        finally; have "... < ..."; .; thus False; ..;
    8.11      qed;
     9.1 --- a/src/HOL/Lambda/Eta.thy	Tue Sep 12 19:03:13 2000 +0200
     9.2 +++ b/src/HOL/Lambda/Eta.thy	Tue Sep 12 22:13:23 2000 +0200
     9.3 @@ -45,7 +45,7 @@
     9.4  
     9.5  subsection "Properties of eta, subst and free"
     9.6  
     9.7 -lemma subst_not_free [rulified, simp]:
     9.8 +lemma subst_not_free [rule_format, simp]:
     9.9      "\<forall>i t u. \<not> free s i --> s[t/i] = s[u/i]"
    9.10    apply (induct_tac s)
    9.11      apply (simp_all add: subst_Var)
    9.12 @@ -74,7 +74,7 @@
    9.13    apply simp_all
    9.14    done
    9.15  
    9.16 -lemma free_eta [rulified]:
    9.17 +lemma free_eta [rule_format]:
    9.18      "s -e> t ==> \<forall>i. free t i = free s i"
    9.19    apply (erule eta.induct)
    9.20       apply (simp_all cong: conj_cong)
    9.21 @@ -85,7 +85,7 @@
    9.22    apply (simp add: free_eta)
    9.23    done
    9.24  
    9.25 -lemma eta_subst [rulified, simp]:
    9.26 +lemma eta_subst [rule_format, simp]:
    9.27      "s -e> t ==> \<forall>u i. s[u/i] -e> t[u/i]"
    9.28    apply (erule eta.induct)
    9.29    apply (simp_all add: subst_subst [symmetric])
    9.30 @@ -136,13 +136,13 @@
    9.31  
    9.32  subsection "Commutation of beta and eta"
    9.33  
    9.34 -lemma free_beta [rulified]:
    9.35 +lemma free_beta [rule_format]:
    9.36      "s -> t ==> \<forall>i. free t i --> free s i"
    9.37    apply (erule beta.induct)
    9.38       apply simp_all
    9.39    done
    9.40  
    9.41 -lemma beta_subst [rulified, intro]:
    9.42 +lemma beta_subst [rule_format, intro]:
    9.43      "s -> t ==> \<forall>u i. s[u/i] -> t[u/i]"
    9.44    apply (erule beta.induct)
    9.45       apply (simp_all add: subst_subst [symmetric])
    9.46 @@ -153,13 +153,13 @@
    9.47    apply (auto elim!: linorder_neqE simp: subst_Var)
    9.48    done
    9.49  
    9.50 -lemma eta_lift [rulified, simp]:
    9.51 +lemma eta_lift [rule_format, simp]:
    9.52      "s -e> t ==> \<forall>i. lift s i -e> lift t i"
    9.53    apply (erule eta.induct)
    9.54       apply simp_all
    9.55    done
    9.56  
    9.57 -lemma rtrancl_eta_subst [rulified]:
    9.58 +lemma rtrancl_eta_subst [rule_format]:
    9.59      "\<forall>s t i. s -e> t --> u[s/i] -e>> u[t/i]"
    9.60    apply (induct_tac u)
    9.61      apply (simp_all add: subst_Var)
    9.62 @@ -190,7 +190,7 @@
    9.63  
    9.64  text {* @{term "Abs (lift s 0 $ Var 0) -e> s"} *}
    9.65  
    9.66 -lemma not_free_iff_lifted [rulified]:
    9.67 +lemma not_free_iff_lifted [rule_format]:
    9.68      "\<forall>i. (\<not> free s i) = (\<exists>t. s = lift t i)"
    9.69    apply (induct_tac s)
    9.70      apply simp
    10.1 --- a/src/HOL/Lambda/InductTermi.thy	Tue Sep 12 19:03:13 2000 +0200
    10.2 +++ b/src/HOL/Lambda/InductTermi.thy	Tue Sep 12 22:13:23 2000 +0200
    10.3 @@ -26,7 +26,7 @@
    10.4  
    10.5  subsection {* Every term in IT terminates *}
    10.6  
    10.7 -lemma double_induction_lemma [rulified]:
    10.8 +lemma double_induction_lemma [rule_format]:
    10.9    "s : termi beta ==> \<forall>t. t : termi beta -->
   10.10      (\<forall>r ss. t = r[s/0] $$ ss --> Abs r $ s $$ ss : termi beta)"
   10.11    apply (erule acc_induct)
    11.1 --- a/src/HOL/Lambda/Lambda.thy	Tue Sep 12 19:03:13 2000 +0200
    11.2 +++ b/src/HOL/Lambda/Lambda.thy	Tue Sep 12 22:13:23 2000 +0200
    11.3 @@ -120,7 +120,7 @@
    11.4    apply (simp add: subst_Var)
    11.5    done
    11.6  
    11.7 -lemma lift_lift [rulified]:
    11.8 +lemma lift_lift [rule_format]:
    11.9      "\<forall>i k. i < k + 1 --> lift (lift t i) (Suc k) = lift (lift t k) i"
   11.10    apply (induct_tac t)
   11.11      apply auto
   11.12 @@ -144,7 +144,7 @@
   11.13      apply simp_all
   11.14    done
   11.15  
   11.16 -lemma subst_subst [rulified]:
   11.17 +lemma subst_subst [rule_format]:
   11.18      "\<forall>i j u v. i < j + 1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
   11.19    apply (induct_tac t)
   11.20      apply (simp_all
   11.21 @@ -183,19 +183,19 @@
   11.22  text {* Not used in Church-Rosser proof, but in Strong
   11.23    Normalization. \medskip *}
   11.24  
   11.25 -theorem subst_preserves_beta [rulified, simp]:
   11.26 +theorem subst_preserves_beta [rule_format, simp]:
   11.27      "r -> s ==> \<forall>t i. r[t/i] -> s[t/i]"
   11.28    apply (erule beta.induct)
   11.29       apply (simp_all add: subst_subst [symmetric])
   11.30    done
   11.31  
   11.32 -theorem lift_preserves_beta [rulified, simp]:
   11.33 +theorem lift_preserves_beta [rule_format, simp]:
   11.34      "r -> s ==> \<forall>i. lift r i -> lift s i"
   11.35    apply (erule beta.induct)
   11.36       apply auto
   11.37    done
   11.38  
   11.39 -theorem subst_preserves_beta2 [rulified, simp]:
   11.40 +theorem subst_preserves_beta2 [rule_format, simp]:
   11.41      "\<forall>r s i. r -> s --> t[r/i] ->> t[s/i]"
   11.42    apply (induct_tac t)
   11.43      apply (simp add: subst_Var r_into_rtrancl)
    12.1 --- a/src/HOL/Lambda/ListApplication.thy	Tue Sep 12 19:03:13 2000 +0200
    12.2 +++ b/src/HOL/Lambda/ListApplication.thy	Tue Sep 12 22:13:23 2000 +0200
    12.3 @@ -18,13 +18,13 @@
    12.4     apply auto
    12.5    done
    12.6  
    12.7 -lemma Var_eq_apps_conv [rulified, iff]:
    12.8 +lemma Var_eq_apps_conv [rule_format, iff]:
    12.9      "\<forall>s. (Var m = s $$ ss) = (Var m = s \<and> ss = [])"
   12.10    apply (induct_tac ss)
   12.11     apply auto
   12.12    done
   12.13  
   12.14 -lemma Var_apps_eq_Var_apps_conv [rulified, iff]:
   12.15 +lemma Var_apps_eq_Var_apps_conv [rule_format, iff]:
   12.16      "\<forall>ss. (Var m $$ rs = Var n $$ ss) = (m = n \<and> rs = ss)"
   12.17    apply (induct_tac rs rule: rev_induct)
   12.18     apply simp
   12.19 @@ -69,7 +69,7 @@
   12.20     apply auto
   12.21    done
   12.22  
   12.23 -lemma Var_apps_neq_Abs_apps [rulified, iff]:
   12.24 +lemma Var_apps_neq_Abs_apps [rule_format, iff]:
   12.25      "\<forall>ts. Var n $$ ts ~= Abs r $$ ss"
   12.26    apply (induct_tac ss rule: rev_induct)
   12.27     apply simp
   12.28 @@ -103,7 +103,7 @@
   12.29  
   12.30  text {* \medskip A customized induction schema for @{text "$$"}. *}
   12.31  
   12.32 -lemma lem [rulified (no_asm)]:
   12.33 +lemma lem [rule_format (no_asm)]:
   12.34    "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
   12.35      !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
   12.36    |] ==> \<forall>t. size t = n --> P t"
    13.1 --- a/src/HOL/Lambda/ListBeta.thy	Tue Sep 12 19:03:13 2000 +0200
    13.2 +++ b/src/HOL/Lambda/ListBeta.thy	Tue Sep 12 22:13:23 2000 +0200
    13.3 @@ -96,7 +96,7 @@
    13.4    apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
    13.5    done
    13.6  
    13.7 -lemma apps_preserves_betas [rulified, simp]:
    13.8 +lemma apps_preserves_betas [rule_format, simp]:
    13.9      "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss"
   13.10    apply (induct_tac rs rule: rev_induct)
   13.11     apply simp
    14.1 --- a/src/HOL/Lambda/ListOrder.thy	Tue Sep 12 19:03:13 2000 +0200
    14.2 +++ b/src/HOL/Lambda/ListOrder.thy	Tue Sep 12 22:13:23 2000 +0200
    14.3 @@ -64,7 +64,7 @@
    14.4    apply (blast intro: append_eq_appendI)
    14.5    done
    14.6  
    14.7 -lemma Cons_step1E [rulified, elim!]:
    14.8 +lemma Cons_step1E [rule_format, elim!]:
    14.9    "[| (ys, x # xs) \<in> step1 r;
   14.10      \<forall>y. ys = y # xs --> (y, x) \<in> r --> R;
   14.11      \<forall>zs. ys = x # zs --> (zs, xs) \<in> step1 r --> R
   14.12 @@ -87,7 +87,7 @@
   14.13    apply blast
   14.14    done
   14.15  
   14.16 -lemma Cons_acc_step1I [rulified, intro!]:
   14.17 +lemma Cons_acc_step1I [rule_format, intro!]:
   14.18      "x \<in> acc r ==> \<forall>xs. xs \<in> acc (step1 r) --> x # xs \<in> acc (step1 r)"
   14.19    apply (erule acc_induct)
   14.20    apply (erule thin_rl)
    15.1 --- a/src/HOL/Lambda/ParRed.thy	Tue Sep 12 19:03:13 2000 +0200
    15.2 +++ b/src/HOL/Lambda/ParRed.thy	Tue Sep 12 22:13:23 2000 +0200
    15.3 @@ -70,13 +70,13 @@
    15.4  
    15.5  subsection {* Misc properties of par-beta *}
    15.6  
    15.7 -lemma par_beta_lift [rulified, simp]:
    15.8 +lemma par_beta_lift [rule_format, simp]:
    15.9      "\<forall>t' n. t => t' --> lift t n => lift t' n"
   15.10    apply (induct_tac t)
   15.11      apply fastsimp+
   15.12    done
   15.13  
   15.14 -lemma par_beta_subst [rulified]:
   15.15 +lemma par_beta_subst [rule_format]:
   15.16      "\<forall>s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]"
   15.17    apply (induct_tac t)
   15.18      apply (simp add: subst_Var)
   15.19 @@ -110,7 +110,7 @@
   15.20    "cd (Abs u $ t) = (cd u)[cd t/0]"
   15.21    "cd (Abs s) = Abs (cd s)"
   15.22  
   15.23 -lemma par_beta_cd [rulified]:
   15.24 +lemma par_beta_cd [rule_format]:
   15.25      "\<forall>t. s => t --> t => cd s"
   15.26    apply (induct_tac s rule: cd.induct)
   15.27        apply auto
    16.1 --- a/src/HOL/Lambda/Type.thy	Tue Sep 12 19:03:13 2000 +0200
    16.2 +++ b/src/HOL/Lambda/Type.thy	Tue Sep 12 22:13:23 2000 +0200
    16.3 @@ -74,7 +74,7 @@
    16.4  
    16.5  text {* Iterated function types *}
    16.6  
    16.7 -lemma list_app_typeD [rulified]:
    16.8 +lemma list_app_typeD [rule_format]:
    16.9      "\<forall>t T. e |- t $$ ts : T --> (\<exists>Ts. e |- t : Ts =>> T \<and> types e ts Ts)"
   16.10    apply (induct_tac ts)
   16.11     apply simp
   16.12 @@ -90,7 +90,7 @@
   16.13    apply simp
   16.14    done
   16.15  
   16.16 -lemma list_app_typeI [rulified]:
   16.17 +lemma list_app_typeI [rule_format]:
   16.18      "\<forall>t T Ts. e |- t : Ts =>> T --> types e ts Ts --> e |- t $$ ts : T"
   16.19    apply (induct_tac ts)
   16.20     apply (intro strip)
   16.21 @@ -109,7 +109,7 @@
   16.22    apply blast
   16.23    done
   16.24  
   16.25 -lemma lists_types [rulified]:
   16.26 +lemma lists_types [rule_format]:
   16.27      "\<forall>Ts. types e ts Ts --> ts \<in> lists {t. \<exists>T. e |- t : T}"
   16.28    apply (induct_tac ts)
   16.29     apply (intro strip)
   16.30 @@ -129,19 +129,19 @@
   16.31  
   16.32  subsection {* Lifting preserves termination and well-typedness *}
   16.33  
   16.34 -lemma lift_map [rulified, simp]:
   16.35 +lemma lift_map [rule_format, simp]:
   16.36      "\<forall>t. lift (t $$ ts) i = lift t i $$ map (\<lambda>t. lift t i) ts"
   16.37    apply (induct_tac ts)
   16.38     apply simp_all
   16.39    done
   16.40  
   16.41 -lemma subst_map [rulified, simp]:
   16.42 +lemma subst_map [rule_format, simp]:
   16.43    "\<forall>t. subst (t $$ ts) u i = subst t u i $$ map (\<lambda>t. subst t u i) ts"
   16.44    apply (induct_tac ts)
   16.45     apply simp_all
   16.46    done
   16.47  
   16.48 -lemma lift_IT [rulified, intro!]:
   16.49 +lemma lift_IT [rule_format, intro!]:
   16.50      "t \<in> IT ==> \<forall>i. lift t i \<in> IT"
   16.51    apply (erule IT.induct)
   16.52      apply (rule allI)
   16.53 @@ -161,7 +161,7 @@
   16.54       apply auto
   16.55     done
   16.56  
   16.57 -lemma lifts_IT [rulified]:
   16.58 +lemma lifts_IT [rule_format]:
   16.59      "ts \<in> lists IT --> map (\<lambda>t. lift t 0) ts \<in> lists IT"
   16.60    apply (induct_tac ts)
   16.61     apply auto
   16.62 @@ -180,7 +180,7 @@
   16.63     apply simp_all
   16.64    done
   16.65  
   16.66 -lemma lift_type' [rulified]:
   16.67 +lemma lift_type' [rule_format]:
   16.68    "e |- t : T ==> \<forall>i U.
   16.69      (\<lambda>j. if j < i then e j
   16.70            else if j = i then U
   16.71 @@ -202,7 +202,7 @@
   16.72     apply simp_all
   16.73    done
   16.74  
   16.75 -lemma lift_types [rulified]:
   16.76 +lemma lift_types [rule_format]:
   16.77    "\<forall>Ts. types e ts Ts -->
   16.78      types (\<lambda>j. if j < i then e j
   16.79                  else if j = i then U
   16.80 @@ -219,7 +219,7 @@
   16.81  
   16.82  subsection {* Substitution lemmas *}
   16.83  
   16.84 -lemma subst_lemma [rulified]:
   16.85 +lemma subst_lemma [rule_format]:
   16.86    "e |- t : T ==> \<forall>e' i U u.
   16.87      e = (\<lambda>j. if j < i then e' j
   16.88                else if j = i then U
   16.89 @@ -242,7 +242,7 @@
   16.90    apply fastsimp
   16.91    done
   16.92  
   16.93 -lemma substs_lemma [rulified]:
   16.94 +lemma substs_lemma [rule_format]:
   16.95    "e |- u : T ==>
   16.96      \<forall>Ts. types (\<lambda>j. if j < i then e j
   16.97                       else if j = i then T else e (j - 1)) ts Ts -->
   16.98 @@ -265,7 +265,7 @@
   16.99  
  16.100  subsection {* Subject reduction *}
  16.101  
  16.102 -lemma subject_reduction [rulified]:
  16.103 +lemma subject_reduction [rule_format]:
  16.104      "e |- t : T ==> \<forall>t'. t -> t' --> e |- t' : T"
  16.105    apply (erule typing.induct)
  16.106      apply blast
  16.107 @@ -290,7 +290,7 @@
  16.108    apply simp
  16.109    done
  16.110  
  16.111 -lemma subst_Var_IT [rulified]: "r \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT"
  16.112 +lemma subst_Var_IT [rule_format]: "r \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT"
  16.113    apply (erule IT.induct)
  16.114      txt {* Case @{term Var}: *}
  16.115      apply (intro strip)
  16.116 @@ -347,7 +347,7 @@
  16.117  
  16.118  subsection {* Well-typed substitution preserves termination *}
  16.119  
  16.120 -lemma subst_type_IT [rulified]:
  16.121 +lemma subst_type_IT [rule_format]:
  16.122    "\<forall>t. t \<in> IT --> (\<forall>e T u i.
  16.123      (\<lambda>j. if j < i then e j
  16.124            else if j = i then U
    17.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Sep 12 19:03:13 2000 +0200
    17.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Sep 12 22:13:23 2000 +0200
    17.3 @@ -587,7 +587,7 @@
    17.4  by (auto simp add: correct_state_def Let_def)
    17.5  
    17.6  
    17.7 -lemma BV_correct_1 [rulified]:
    17.8 +lemma BV_correct_1 [rule_format]:
    17.9  "\<And>state. \<lbrakk> wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>\<rbrakk> 
   17.10   \<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   17.11  apply (simp only: split_tupled_all)
   17.12 @@ -617,7 +617,7 @@
   17.13  done
   17.14  
   17.15  
   17.16 -theorem BV_correct [rulified]:
   17.17 +theorem BV_correct [rule_format]:
   17.18  "\<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>"
   17.19  apply (unfold exec_all_def)
   17.20  apply (erule rtrancl_induct)
    18.1 --- a/src/HOL/MicroJava/BV/Convert.thy	Tue Sep 12 19:03:13 2000 +0200
    18.2 +++ b/src/HOL/MicroJava/BV/Convert.thy	Tue Sep 12 22:13:23 2000 +0200
    18.3 @@ -383,7 +383,7 @@
    18.4  qed
    18.5  
    18.6  
    18.7 -theorem sup_loc_update [rulified]:
    18.8 +theorem sup_loc_update [rule_format]:
    18.9    "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow> 
   18.10            (G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x")
   18.11  proof (induct x)
   18.12 @@ -485,7 +485,7 @@
   18.13  
   18.14    with G
   18.15    show ?thesis 
   18.16 -    by (auto intro!: all_nth_sup_loc [rulified] dest!: sup_loc_length) 
   18.17 +    by (auto intro!: all_nth_sup_loc [rule_format] dest!: sup_loc_length) 
   18.18  qed
   18.19    
   18.20  
    19.1 --- a/src/HOL/MicroJava/BV/Correct.thy	Tue Sep 12 19:03:13 2000 +0200
    19.2 +++ b/src/HOL/MicroJava/BV/Correct.thy	Tue Sep 12 22:13:23 2000 +0200
    19.3 @@ -92,11 +92,11 @@
    19.4    "approx_val G hp Null (Ok (RefT x))"
    19.5  by (auto intro: null simp add: approx_val_def)
    19.6  
    19.7 -lemma approx_val_imp_approx_val_assConvertible [rulified]: 
    19.8 +lemma approx_val_imp_approx_val_assConvertible [rule_format]: 
    19.9    "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')"
   19.10  by (cases T) (auto intro: conf_widen simp add: approx_val_def)
   19.11  
   19.12 -lemma approx_val_imp_approx_val_sup_heap [rulified]:
   19.13 +lemma approx_val_imp_approx_val_sup_heap [rule_format]:
   19.14    "approx_val G hp v at \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_val G hp' v at"
   19.15  apply (simp add: approx_val_def split: err.split)
   19.16  apply (blast intro: conf_hext)
   19.17 @@ -107,7 +107,7 @@
   19.18    \<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v\<Colon>\<preceq>T"
   19.19  by (cases v, auto simp add: obj_ty_def conf_def)
   19.20  
   19.21 -lemma approx_val_imp_approx_val_sup [rulified]:
   19.22 +lemma approx_val_imp_approx_val_sup [rule_format]:
   19.23    "wf_prog wt G \<Longrightarrow> (approx_val G h v us) \<longrightarrow> (G \<turnstile> us <=o us') \<longrightarrow> (approx_val G h v us')"
   19.24  apply (simp add: sup_PTS_eq approx_val_def split: err.split)
   19.25  apply (blast intro: conf_widen)
   19.26 @@ -128,7 +128,7 @@
   19.27    "approx_loc G hp (s#xs) (l#ls) = (approx_val G hp s l \<and> approx_loc G hp xs ls)"
   19.28  by (simp add: approx_loc_def)
   19.29  
   19.30 -lemma assConv_approx_stk_imp_approx_loc [rulified]:
   19.31 +lemma assConv_approx_stk_imp_approx_loc [rule_format]:
   19.32    "wf_prog wt G \<Longrightarrow> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G) 
   19.33    \<longrightarrow> length tys_n = length ts \<longrightarrow> approx_stk G hp s tys_n \<longrightarrow> 
   19.34    approx_loc G hp s (map Ok ts)"
   19.35 @@ -139,7 +139,7 @@
   19.36  .
   19.37  
   19.38  
   19.39 -lemma approx_loc_imp_approx_loc_sup_heap [rulified]:
   19.40 +lemma approx_loc_imp_approx_loc_sup_heap [rule_format]:
   19.41    "\<forall>lvars. approx_loc G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_loc G hp' lvars lt"
   19.42  apply (unfold approx_loc_def list_all2_def)
   19.43  apply (cases lt)
   19.44 @@ -149,7 +149,7 @@
   19.45  apply auto
   19.46  .
   19.47  
   19.48 -lemma approx_loc_imp_approx_loc_sup [rulified]:
   19.49 +lemma approx_loc_imp_approx_loc_sup [rule_format]:
   19.50    "wf_prog wt G \<Longrightarrow> approx_loc G hp lvars lt \<longrightarrow> G \<turnstile> lt <=l lt' \<longrightarrow> approx_loc G hp lvars lt'"
   19.51  apply (unfold sup_loc_def approx_loc_def list_all2_def)
   19.52  apply (auto simp add: all_set_conv_all_nth)
   19.53 @@ -157,7 +157,7 @@
   19.54  .
   19.55  
   19.56  
   19.57 -lemma approx_loc_imp_approx_loc_subst [rulified]:
   19.58 +lemma approx_loc_imp_approx_loc_subst [rule_format]:
   19.59    "\<forall>loc idx x X. (approx_loc G hp loc LT) \<longrightarrow> (approx_val G hp x X) 
   19.60    \<longrightarrow> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))"
   19.61  apply (unfold approx_loc_def list_all2_def)
   19.62 @@ -167,7 +167,7 @@
   19.63  
   19.64  lemmas [cong] = conj_cong 
   19.65  
   19.66 -lemma approx_loc_append [rulified]:
   19.67 +lemma approx_loc_append [rule_format]:
   19.68    "\<forall>L1 l2 L2. length l1=length L1 \<longrightarrow> 
   19.69    approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
   19.70  apply (unfold approx_loc_def list_all2_def)
   19.71 @@ -191,11 +191,11 @@
   19.72  by (auto intro: subst [OF approx_stk_rev_lem])
   19.73  
   19.74  
   19.75 -lemma approx_stk_imp_approx_stk_sup_heap [rulified]:
   19.76 +lemma approx_stk_imp_approx_stk_sup_heap [rule_format]:
   19.77    "\<forall>lvars. approx_stk G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_stk G hp' lvars lt"
   19.78  by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def)
   19.79  
   19.80 -lemma approx_stk_imp_approx_stk_sup [rulified]:
   19.81 +lemma approx_stk_imp_approx_stk_sup [rule_format]:
   19.82    "wf_prog wt G \<Longrightarrow> approx_stk G hp lvars st \<longrightarrow> (G \<turnstile> map Ok st <=l (map Ok st')) 
   19.83    \<longrightarrow> approx_stk G hp lvars st'" 
   19.84  by (auto intro: approx_loc_imp_approx_loc_sup simp add: approx_stk_def)
   19.85 @@ -232,13 +232,13 @@
   19.86  .
   19.87  
   19.88  
   19.89 -lemma oconf_imp_oconf_field_update [rulified]:
   19.90 +lemma oconf_imp_oconf_field_update [rule_format]:
   19.91    "\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v\<Colon>\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
   19.92    \<Longrightarrow> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
   19.93  by (simp add: oconf_def lconf_def)
   19.94  
   19.95  
   19.96 -lemma oconf_imp_oconf_heap_newref [rulified]:
   19.97 +lemma oconf_imp_oconf_heap_newref [rule_format]:
   19.98  "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>"
   19.99  apply (unfold oconf_def lconf_def)
  19.100  apply simp
  19.101 @@ -246,7 +246,7 @@
  19.102  .
  19.103  
  19.104  
  19.105 -lemma oconf_imp_oconf_heap_update [rulified]:
  19.106 +lemma oconf_imp_oconf_heap_update [rule_format]:
  19.107    "hp a = Some obj' \<longrightarrow> obj_ty obj' = obj_ty obj'' \<longrightarrow> G,hp\<turnstile>obj\<surd> 
  19.108    \<longrightarrow> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
  19.109  apply (unfold oconf_def lconf_def)
  19.110 @@ -258,13 +258,13 @@
  19.111  (** hconf **)
  19.112  
  19.113  
  19.114 -lemma hconf_imp_hconf_newref [rulified]:
  19.115 +lemma hconf_imp_hconf_newref [rule_format]:
  19.116    "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>"
  19.117  apply (simp add: hconf_def)
  19.118  apply (fast intro: oconf_imp_oconf_heap_newref)
  19.119  .
  19.120  
  19.121 -lemma hconf_imp_hconf_field_update [rulified]:
  19.122 +lemma hconf_imp_hconf_field_update [rule_format]:
  19.123    "map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and> 
  19.124    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>"
  19.125  apply (simp add: hconf_def)
  19.126 @@ -276,7 +276,7 @@
  19.127  
  19.128  lemmas [simp del] = fun_upd_apply
  19.129  
  19.130 -lemma correct_frames_imp_correct_frames_field_update [rulified]:
  19.131 +lemma correct_frames_imp_correct_frames_field_update [rule_format]:
  19.132    "\<forall>rT C sig. correct_frames G hp phi rT sig frs \<longrightarrow> 
  19.133    hp a = Some (C,od) \<longrightarrow> map_of (fields (G, C)) fl = Some fd \<longrightarrow> 
  19.134    G,hp\<turnstile>v\<Colon>\<preceq>fd 
  19.135 @@ -299,7 +299,7 @@
  19.136  apply simp
  19.137  .
  19.138  
  19.139 -lemma correct_frames_imp_correct_frames_newref [rulified]:
  19.140 +lemma correct_frames_imp_correct_frames_newref [rule_format]:
  19.141    "\<forall>rT C sig. hp x = None \<longrightarrow> correct_frames G hp phi rT sig frs \<and> oconf G hp obj 
  19.142    \<longrightarrow> correct_frames G (hp(newref hp \<mapsto> obj)) phi rT sig frs"
  19.143  apply (induct frs)
    20.1 --- a/src/HOL/MicroJava/BV/LBVComplete.thy	Tue Sep 12 19:03:13 2000 +0200
    20.2 +++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Tue Sep 12 22:13:23 2000 +0200
    20.3 @@ -161,7 +161,7 @@
    20.4      case None
    20.5      with wtl fits
    20.6      show ?thesis 
    20.7 -      by - (rule wtl_inst_mono [elimified], (simp add: wtl_cert_def)+)
    20.8 +      by - (rule wtl_inst_mono [elim_format], (simp add: wtl_cert_def)+)
    20.9    next
   20.10      case Some
   20.11      with wtl fits
   20.12 @@ -406,7 +406,7 @@
   20.13    "[| wt_method G C pTs rT mxl ins phi; fits ins cert phi |] ==> 
   20.14    wtl_method G C pTs rT mxl ins cert"
   20.15  by (simp add: wt_method_def wtl_method_def)
   20.16 -   (rule wt_imp_wtl_inst_list [rulified, elimified], auto simp add: wt_start_def) 
   20.17 +   (rule wt_imp_wtl_inst_list [rule_format, elim_format], auto simp add: wt_start_def) 
   20.18  
   20.19  
   20.20  lemma wtl_method_complete:
   20.21 @@ -462,17 +462,17 @@
   20.22  
   20.23      from 1
   20.24      show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))"
   20.25 -    proof (rule bspec [elimified], clarsimp)
   20.26 +    proof (rule bspec [elim_format], clarsimp)
   20.27        assume ub : "unique b"
   20.28        assume m: "\<forall>(sig,rT,mb)\<in>set b. wf_mhead G sig rT \<and> 
   20.29                    (\<lambda>(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb" 
   20.30        from m b
   20.31        show ?thesis
   20.32 -      proof (rule bspec [elimified], clarsimp)
   20.33 +      proof (rule bspec [elim_format], clarsimp)
   20.34          assume "wt_method G a ba ad ae bb (Phi a (ac, ba))"         
   20.35          with wfprog uG ub b 1
   20.36          show ?thesis
   20.37 -          by - (rule wtl_method_complete [elimified], assumption+, 
   20.38 +          by - (rule wtl_method_complete [elim_format], assumption+, 
   20.39                  simp add: make_Cert_def unique_epsilon)
   20.40        qed 
   20.41      qed
    21.1 --- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Tue Sep 12 19:03:13 2000 +0200
    21.2 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Tue Sep 12 22:13:23 2000 +0200
    21.3 @@ -264,7 +264,7 @@
    21.4    assume wtl: "wtl_inst_list ins G rT cert (length ins) 0 ?s0 \<noteq> Err"
    21.5  
    21.6    obtain phi where fits: "fits phi ins G rT ?s0 cert"    
    21.7 -    by (rule exists_phi [elimified]) blast
    21.8 +    by (rule exists_phi [elim_format]) blast
    21.9  
   21.10    with wtl
   21.11    have allpc:
    22.1 --- a/src/HOL/MicroJava/BV/StepMono.thy	Tue Sep 12 19:03:13 2000 +0200
    22.2 +++ b/src/HOL/MicroJava/BV/StepMono.thy	Tue Sep 12 22:13:23 2000 +0200
    22.3 @@ -13,7 +13,7 @@
    22.4    by (auto elim: widen.elims)
    22.5  
    22.6  
    22.7 -lemma sup_loc_some [rulified]:
    22.8 +lemma sup_loc_some [rule_format]:
    22.9  "\<forall> y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = Ok t \<longrightarrow> 
   22.10    (\<exists>t. b!n = Ok t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
   22.11  proof (induct (open) ?P b)
   22.12 @@ -59,7 +59,7 @@
   22.13  qed
   22.14   
   22.15  
   22.16 -lemma append_length_n [rulified]: 
   22.17 +lemma append_length_n [rule_format]: 
   22.18  "\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
   22.19  proof (induct (open) ?P x)
   22.20    show "?P []" by simp
   22.21 @@ -78,7 +78,7 @@
   22.22        fix "n'" assume s: "n = Suc n'"
   22.23        with l 
   22.24        have  "n' \<le> length ls" by simp 
   22.25 -      hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rulified])
   22.26 +      hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rule_format])
   22.27        thus ?thesis
   22.28        proof elim
   22.29          fix a b 
   22.30 @@ -254,7 +254,7 @@
   22.31          have "length list < length (fst s2)" 
   22.32            by (simp add: sup_state_length)
   22.33          hence "\<exists>a b c. (fst s2) = rev a @ b # c \<and> length a = length list"
   22.34 -          by (rule rev_append_cons [rulified])
   22.35 +          by (rule rev_append_cons [rule_format])
   22.36          thus ?thesis
   22.37            by -  (cases s2, elim exE conjE, simp, rule that) 
   22.38        qed
    23.1 --- a/src/HOL/Real/HahnBanach/Aux.thy	Tue Sep 12 19:03:13 2000 +0200
    23.2 +++ b/src/HOL/Real/HahnBanach/Aux.thy	Tue Sep 12 22:13:23 2000 +0200
    23.3 @@ -12,7 +12,7 @@
    23.4  
    23.5  lemmas [intro?] = isLub_isUb
    23.6  lemmas [intro?] = chainD 
    23.7 -lemmas chainE2 = chainD2 [elimified]
    23.8 +lemmas chainE2 = chainD2 [elim_format, standard]
    23.9  
   23.10  text_raw {* \medskip *}
   23.11  text{* Lemmas about sets. *}
    24.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Tue Sep 12 19:03:13 2000 +0200
    24.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Tue Sep 12 22:13:23 2000 +0200
    24.3 @@ -227,7 +227,7 @@
    24.4    "x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)"
    24.5      by (unfold vs_sum_def) fast
    24.6  
    24.7 -lemmas vs_sumE = vs_sumD [THEN iffD1, elimified, standard]
    24.8 +lemmas vs_sumE = vs_sumD [THEN iffD1, elim_format, standard]
    24.9  
   24.10  lemma vs_sumI [intro?]: 
   24.11    "[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V"
    25.1 --- a/src/HOL/ex/Primes.thy	Tue Sep 12 19:03:13 2000 +0200
    25.2 +++ b/src/HOL/ex/Primes.thy	Tue Sep 12 22:13:23 2000 +0200
    25.3 @@ -71,7 +71,7 @@
    25.4  
    25.5  (*Maximality: for all m,n,k naturals, 
    25.6                  if k divides m and k divides n then k divides gcd(m,n)*)
    25.7 -lemma gcd_greatest [rulified]: "(k dvd m) --> (k dvd n) --> k dvd gcd(m,n)"
    25.8 +lemma gcd_greatest [rule_format]: "(k dvd m) --> (k dvd n) --> k dvd gcd(m,n)"
    25.9    apply (induct_tac m n rule: gcd_induct)
   25.10    apply (simp_all add: gcd_non_0 dvd_mod);
   25.11    done;
    26.1 --- a/src/Provers/classical.ML	Tue Sep 12 19:03:13 2000 +0200
    26.2 +++ b/src/Provers/classical.ML	Tue Sep 12 22:13:23 2000 +0200
    26.3 @@ -1046,10 +1046,11 @@
    26.4  
    26.5  (* setup_attrs *)
    26.6  
    26.7 -fun elimified x = Attrib.no_args (Drule.rule_attribute (K Data.make_elim)) x;
    26.8 +fun elim_format x = Attrib.no_args (Drule.rule_attribute (K Data.make_elim)) x;
    26.9  
   26.10  val setup_attrs = Attrib.add_attributes
   26.11 - [("elimified", (elimified, elimified), "destruct rule turned into elimination rule (classical)"),
   26.12 + [("elim_format", (elim_format, elim_format),
   26.13 +    "destruct rule turned into elimination rule format (classical)"),
   26.14    (destN, cla_attr (op addXDs) (op addDs) (op addSDs), "declaration of destruction rule"),
   26.15    (elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "declaration of elimination rule"),
   26.16    (introN, cla_attr (op addXIs) (op addIs) (op addSIs), "declaration of introduction rule"),
    27.1 --- a/src/Provers/rulify.ML	Tue Sep 12 19:03:13 2000 +0200
    27.2 +++ b/src/Provers/rulify.ML	Tue Sep 12 22:13:23 2000 +0200
    27.3 @@ -19,8 +19,8 @@
    27.4  signature RULIFY =
    27.5  sig
    27.6    include BASIC_RULIFY
    27.7 -  val rulified: 'a attribute
    27.8 -  val rulified_no_asm: 'a attribute
    27.9 +  val rule_format: 'a attribute
   27.10 +  val rule_format_no_asm: 'a attribute
   27.11    val setup: (theory -> theory) list
   27.12  end;
   27.13  
   27.14 @@ -38,11 +38,11 @@
   27.15  
   27.16  (* attributes *)
   27.17  
   27.18 -fun rulified x = Drule.rule_attribute (fn _ => rulify) x;
   27.19 -fun rulified_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
   27.20 +fun rule_format x = Drule.rule_attribute (fn _ => rulify) x;
   27.21 +fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
   27.22  
   27.23 -fun rulified_att x = Attrib.syntax
   27.24 -  (Scan.lift (Args.parens (Args.$$$ "no_asm") >> K rulified_no_asm || Scan.succeed rulified)) x;
   27.25 +fun rule_format_att x = Attrib.syntax
   27.26 +  (Scan.lift (Args.parens (Args.$$$ "no_asm") >> K rule_format_no_asm || Scan.succeed rule_format)) x;
   27.27  
   27.28  
   27.29  (* qed commands *)
   27.30 @@ -60,6 +60,6 @@
   27.31  
   27.32  val setup =
   27.33   [Attrib.add_attributes
   27.34 -  [("rulified", (rulified_att, rulified_att), "result put into standard rule form")]];
   27.35 +  [("rule_format", (rule_format_att, rule_format_att), "result put into standard rule format")]];
   27.36  
   27.37  end;
    28.1 --- a/src/Pure/Isar/attrib.ML	Tue Sep 12 19:03:13 2000 +0200
    28.2 +++ b/src/Pure/Isar/attrib.ML	Tue Sep 12 22:13:23 2000 +0200
    28.3 @@ -269,7 +269,7 @@
    28.4  (* misc rules *)
    28.5  
    28.6  fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) x;
    28.7 -fun elimified x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x;
    28.8 +fun elim_format x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x;
    28.9  fun no_vars x = no_args (Drule.rule_attribute (K (#1 o Drule.freeze_thaw))) x;
   28.10  
   28.11  fun exported_global x = no_args (Drule.rule_attribute (Proof.export_thm o ProofContext.init)) x;
   28.12 @@ -292,7 +292,7 @@
   28.13    ("unfolded", (unfolded_global, unfolded_local), "unfolded definitions"),
   28.14    ("folded", (folded_global, folded_local), "folded definitions"),
   28.15    ("standard", (standard, standard), "result put into standard form"),
   28.16 -  ("elimified", (elimified, elimified), "destruct rule turned into elimination rule"),
   28.17 +  ("elim_format", (elim_format, elim_format), "destruct rule turned into elimination rule format"),
   28.18    ("no_vars", (no_vars, no_vars), "frozen schematic vars"),
   28.19    ("case_names", (case_names, case_names), "named rule cases"),
   28.20    ("params", (params, params), "named rule parameters"),