equal
deleted
inserted
replaced
448 by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1); |
448 by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1); |
449 qed "lessD"; |
449 qed "lessD"; |
450 |
450 |
451 goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n"; |
451 goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n"; |
452 by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1); |
452 by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1); |
453 by (Fast_tac 1); |
|
454 qed "Suc_leD"; |
453 qed "Suc_leD"; |
455 |
454 |
456 (* stronger version of Suc_leD *) |
455 (* stronger version of Suc_leD *) |
457 goalw Nat.thy [le_def] |
456 goalw Nat.thy [le_def] |
458 "!!m. Suc m <= n ==> m < n"; |
457 "!!m. Suc m <= n ==> m < n"; |