--- a/src/HOL/MicroJava/BV/StepMono.thy Sat Aug 19 12:49:19 2000 +0200
+++ b/src/HOL/MicroJava/BV/StepMono.thy Sun Aug 20 17:45:20 2000 +0200
@@ -15,7 +15,7 @@
lemma sup_loc_some [rulify]:
"\<forall> y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = Some t \<longrightarrow> (\<exists>t. b!n = Some t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
-proof (induct "?P" b)
+proof (induct (open) ?P b)
show "?P []" by simp
case Cons
@@ -59,7 +59,7 @@
lemma append_length_n [rulify]:
"\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
-proof (induct "?P" "x")
+proof (induct (open) ?P x)
show "?P []" by simp
fix l ls assume Cons: "?P ls"
@@ -122,7 +122,7 @@
assume app: "app (i, G, rT, s1)"
show ?thesis
- proof (cases i)
+ proof (cases (open) i)
case Load
from G
@@ -308,7 +308,7 @@
by (auto dest!: app_step_some);
have "G \<turnstile> (a1',b1') <=s (a2',b2')"
- proof (cases i)
+ proof (cases (open) i)
case Load
with s app1