src/HOL/MicroJava/BV/StepMono.thy
 changeset 9941 fe05af7ec816 parent 9906 5c027cca6262 child 10042 7164dc0d24d8
```     1.1 --- a/src/HOL/MicroJava/BV/StepMono.thy	Tue Sep 12 19:03:13 2000 +0200
1.2 +++ b/src/HOL/MicroJava/BV/StepMono.thy	Tue Sep 12 22:13:23 2000 +0200
1.3 @@ -13,7 +13,7 @@
1.4    by (auto elim: widen.elims)
1.5
1.6
1.7 -lemma sup_loc_some [rulified]:
1.8 +lemma sup_loc_some [rule_format]:
1.9  "\<forall> y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = Ok t \<longrightarrow>
1.10    (\<exists>t. b!n = Ok t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
1.11  proof (induct (open) ?P b)
1.12 @@ -59,7 +59,7 @@
1.13  qed
1.14
1.15
1.16 -lemma append_length_n [rulified]:
1.17 +lemma append_length_n [rule_format]:
1.18  "\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
1.19  proof (induct (open) ?P x)
1.20    show "?P []" by simp
1.21 @@ -78,7 +78,7 @@
1.22        fix "n'" assume s: "n = Suc n'"
1.23        with l
1.24        have  "n' \<le> length ls" by simp
1.25 -      hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rulified])
1.26 +      hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rule_format])
1.27        thus ?thesis
1.28        proof elim
1.29          fix a b
1.30 @@ -254,7 +254,7 @@
1.31          have "length list < length (fst s2)"