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)" 
    1.32            by (simp add: sup_state_length)
    1.33          hence "\<exists>a b c. (fst s2) = rev a @ b # c \<and> length a = length list"
    1.34 -          by (rule rev_append_cons [rulified])
    1.35 +          by (rule rev_append_cons [rule_format])
    1.36          thus ?thesis
    1.37            by -  (cases s2, elim exE conjE, simp, rule that) 
    1.38        qed