src/HOL/Nat.thy
changeset 61070 b72a990adfe2
parent 60758 d8d85a8172b5
child 61076 bdc1e2f0a86a
     1.1 --- a/src/HOL/Nat.thy	Mon Aug 31 21:01:21 2015 +0200
     1.2 +++ b/src/HOL/Nat.thy	Mon Aug 31 21:28:08 2015 +0200
     1.3 @@ -1588,11 +1588,8 @@
     1.4  context semiring_1
     1.5  begin
     1.6  
     1.7 -definition Nats  :: "'a set" where
     1.8 -  "Nats = range of_nat"
     1.9 -
    1.10 -notation (xsymbols)
    1.11 -  Nats  ("\<nat>")
    1.12 +definition Nats :: "'a set"  ("\<nat>")
    1.13 +  where "\<nat> = range of_nat"
    1.14  
    1.15  lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>"
    1.16    by (simp add: Nats_def)