src/HOL/Real/PNat.ML
changeset 7562 8519d5019309
parent 7292 dff3470c5c62
child 8856 435187ffc64e
     1.1 --- a/src/HOL/Real/PNat.ML	Tue Sep 21 17:28:33 1999 +0200
     1.2 +++ b/src/HOL/Real/PNat.ML	Tue Sep 21 17:29:00 1999 +0200
     1.3 @@ -86,8 +86,6 @@
     1.4  by (rtac Rep_pnat_inverse 1);
     1.5  qed "inj_Rep_pnat";
     1.6  
     1.7 -bind_thm ("Zero_not_Suc", Suc_not_Zero RS not_sym);
     1.8 -
     1.9  Goal "0 ~: pnat";
    1.10  by (stac pnat_unfold 1);
    1.11  by Auto_tac;