equal
deleted
inserted
replaced
255 proof - |
255 proof - |
256 have plus_le_conv3: "!!A x y z f r. |
256 have plus_le_conv3: "!!A x y z f r. |
257 [| semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A |] |
257 [| semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A |] |
258 ==> x <=_r z \<and> y <=_r z" |
258 ==> x <=_r z \<and> y <=_r z" |
259 by (rule plus_le_conv [THEN iffD1]) |
259 by (rule plus_le_conv [THEN iffD1]) |
260 case antecedent |
260 case rule_context |
261 thus ?thesis |
261 thus ?thesis |
262 apply (rule_tac iffI) |
262 apply (rule_tac iffI) |
263 apply clarify |
263 apply clarify |
264 apply (drule OK_le_err_OK [THEN iffD2]) |
264 apply (drule OK_le_err_OK [THEN iffD2]) |
265 apply (drule OK_le_err_OK [THEN iffD2]) |
265 apply (drule OK_le_err_OK [THEN iffD2]) |