| changeset 11655 | 923e4d0d36d5 |
| parent 11464 | ddea204de5bc |
| child 11701 | 3d51fbf81c17 |
--- a/src/HOL/Real/PRat.ML Wed Oct 03 20:54:05 2001 +0200 +++ b/src/HOL/Real/PRat.ML Wed Oct 03 20:54:16 2001 +0200 @@ -332,7 +332,7 @@ (* prove introduction and elimination rules for prat_less *) Goalw [prat_less_def] - "Q1 < (Q2::prat) = (EX Q3. Q1 + Q3 = Q2)"; + "(Q1 < (Q2::prat)) = (EX Q3. Q1 + Q3 = Q2)"; by (Fast_tac 1); qed "prat_less_iff";