src/HOL/MicroJava/BV/Convert.thy
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 10042 7164dc0d24d8
     1.1 --- a/src/HOL/MicroJava/BV/Convert.thy	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/Convert.thy	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -383,7 +383,7 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -theorem sup_loc_update [rulified]:
     1.8 +theorem sup_loc_update [rule_format]:
     1.9    "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow> 
    1.10            (G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x")
    1.11  proof (induct x)
    1.12 @@ -485,7 +485,7 @@
    1.13  
    1.14    with G
    1.15    show ?thesis 
    1.16 -    by (auto intro!: all_nth_sup_loc [rulified] dest!: sup_loc_length) 
    1.17 +    by (auto intro!: all_nth_sup_loc [rule_format] dest!: sup_loc_length) 
    1.18  qed
    1.19    
    1.20