| changeset 10231 | 178a272bceeb |
| parent 10202 | 9e8b4bebc940 |
| child 10292 | 19753287b9df |
--- a/src/HOL/Real/PNat.ML Tue Oct 17 10:20:43 2000 +0200 +++ b/src/HOL/Real/PNat.ML Tue Oct 17 10:21:12 2000 +0200 @@ -244,7 +244,7 @@ qed "pnat_less_not_sym"; (* [| x < y; ~P ==> y < x |] ==> P *) -bind_thm ("pnat_less_asym", pnat_less_not_sym RS swap); +bind_thm ("pnat_less_asym", pnat_less_not_sym RS contrapos_np); Goalw [pnat_less_def] "~ y < (y::pnat)"; by Auto_tac;