src/HOL/Nat.ML
changeset 10173 1d097572d23b
parent 9969 4753185f1dd2
child 10450 60ddd5fdf93b
equal deleted inserted replaced
10172:3daeda3d3cd0 10173:1d097572d23b
    56 by(fast_tac (claset() addIs [not0_implies_Suc]) 1);
    56 by(fast_tac (claset() addIs [not0_implies_Suc]) 1);
    57 qed "gr0_conv_Suc";
    57 qed "gr0_conv_Suc";
    58 
    58 
    59 Goal "!!n::nat. (~(0 < n)) = (n=0)";
    59 Goal "!!n::nat. (~(0 < n)) = (n=0)";
    60 by (rtac iffI 1);
    60 by (rtac iffI 1);
    61  by (etac swap 1);
    61  by (rtac ccontr 1);
    62  by (ALLGOALS Asm_full_simp_tac);
    62  by (ALLGOALS Asm_full_simp_tac);
    63 qed "not_gr0";
    63 qed "not_gr0";
    64 AddIffs [not_gr0];
    64 AddIffs [not_gr0];
    65 
    65 
    66 Goal "(Suc n <= m') --> (? m. m' = Suc m)";
    66 Goal "(Suc n <= m') --> (? m. m' = Suc m)";