--- 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