equal
deleted
inserted
replaced
244 |
244 |
245 Goalw [pnat_less_def] "x < (y::pnat) ==> ~ y < x"; |
245 Goalw [pnat_less_def] "x < (y::pnat) ==> ~ y < x"; |
246 by (etac less_not_sym 1); |
246 by (etac less_not_sym 1); |
247 qed "pnat_less_not_sym"; |
247 qed "pnat_less_not_sym"; |
248 |
248 |
249 (* [| x < y; y < x |] ==> P *) |
249 (* [| x < y; ~P ==> y < x |] ==> P *) |
250 bind_thm ("pnat_less_asym",pnat_less_not_sym RS notE); |
250 bind_thm ("pnat_less_asym", pnat_less_not_sym RS swap); |
251 |
251 |
252 Goalw [pnat_less_def] "~ y < (y::pnat)"; |
252 Goalw [pnat_less_def] "~ y < (y::pnat)"; |
253 by Auto_tac; |
253 by Auto_tac; |
254 qed "pnat_less_not_refl"; |
254 qed "pnat_less_not_refl"; |
255 |
255 |