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