equal
deleted
inserted
replaced
77 proof - |
77 proof - |
78 have plus_le_conv2: |
78 have plus_le_conv2: |
79 "!!r f z. [| z : err A; semilat (err A, r, f); OK x : err A; OK y : err A; |
79 "!!r f z. [| z : err A; semilat (err A, r, f); OK x : err A; OK y : err A; |
80 OK x +_f OK y <=_r z|] ==> OK x <=_r z \<and> OK y <=_r z" |
80 OK x +_f OK y <=_r z|] ==> OK x <=_r z \<and> OK y <=_r z" |
81 by (rule plus_le_conv [THEN iffD1]) |
81 by (rule plus_le_conv [THEN iffD1]) |
82 case antecedent |
82 case rule_context |
83 thus ?thesis |
83 thus ?thesis |
84 apply (rule_tac iffI) |
84 apply (rule_tac iffI) |
85 apply clarify |
85 apply clarify |
86 apply (drule OK_le_err_OK [THEN iffD2]) |
86 apply (drule OK_le_err_OK [THEN iffD2]) |
87 apply (drule OK_le_err_OK [THEN iffD2]) |
87 apply (drule OK_le_err_OK [THEN iffD2]) |