author | berghofe |
Fri, 21 Jun 1996 13:51:09 +0200 | |
changeset 1823 | e1458e1a9f80 |
parent 1822 | c192d7dc22e7 |
child 1824 | 44254696843a |
src/HOL/Nat.ML | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Nat.ML Fri Jun 21 13:39:08 1996 +0200 +++ b/src/HOL/Nat.ML Fri Jun 21 13:51:09 1996 +0200 @@ -462,7 +462,7 @@ "!!m. Suc m <= n ==> m < n"; by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1); by (cut_facts_tac [less_linear] 1); -by (fast_tac HOL_cs 1); +by (Fast_tac 1); qed "Suc_le_lessD"; goal Nat.thy "(Suc m <= n) = (m < n)";