src/HOL/Nat.thy
changeset 5714 b4f2e281a907
parent 5499 1787c44ae4ed
child 7702 35c7e0df749f
     1.1 --- a/src/HOL/Nat.thy	Wed Oct 21 16:38:46 1998 +0200
     1.2 +++ b/src/HOL/Nat.thy	Wed Oct 21 17:38:47 1998 +0200
     1.3 @@ -12,8 +12,8 @@
     1.4    DatatypePackage.setup
     1.5  
     1.6  rep_datatype nat
     1.7 -  distinct "[[Suc_not_Zero, Zero_not_Suc]]"
     1.8 -  inject   "[[Suc_Suc_eq]]"
     1.9 +  distinct Suc_not_Zero, Zero_not_Suc
    1.10 +  inject   Suc_Suc_eq
    1.11    induct   nat_induct
    1.12  
    1.13  instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)