equal
deleted
inserted
replaced
37 by (Blast_tac 1); |
37 by (Blast_tac 1); |
38 qed "neq0_conv"; |
38 qed "neq0_conv"; |
39 AddIffs [neq0_conv]; |
39 AddIffs [neq0_conv]; |
40 |
40 |
41 Goal "(0 ~= n) = (0 < n)"; |
41 Goal "(0 ~= n) = (0 < n)"; |
42 by(exhaust_tac "n" 1); |
42 by (exhaust_tac "n" 1); |
43 by(Auto_tac); |
43 by (Auto_tac); |
44 qed "zero_neq_conv"; |
44 qed "zero_neq_conv"; |
45 AddIffs [zero_neq_conv]; |
45 AddIffs [zero_neq_conv]; |
46 |
46 |
47 (*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *) |
47 (*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *) |
48 bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1); |
48 bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1); |