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