changeset 11549 | e7265e70fd7c |
parent 10496 | f2d304bdf3cc |
child 12516 | d09d0f160888 |
--- a/src/HOL/MicroJava/BV/Product.thy Tue Sep 04 17:31:18 2001 +0200 +++ b/src/HOL/MicroJava/BV/Product.thy Tue Sep 04 21:10:57 2001 +0200 @@ -79,7 +79,7 @@ "!!r f z. [| z : err A; semilat (err A, r, f); OK x : err A; OK y : err A; OK x +_f OK y <=_r z|] ==> OK x <=_r z \<and> OK y <=_r z" by (rule plus_le_conv [THEN iffD1]) - case antecedent + case rule_context thus ?thesis apply (rule_tac iffI) apply clarify