--- a/src/HOL/Integ/IntDef.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy Tue May 16 21:33:01 2006 +0200
@@ -567,9 +567,8 @@
Nats :: "'a::comm_semiring_1_cancel set"
"Nats == range of_nat"
-abbreviation (xsymbols)
- Nats1 ("\<nat>")
- "\<nat> == Nats"
+const_syntax (xsymbols)
+ Nats ("\<nat>")
lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats"
by (simp add: Nats_def)
@@ -701,9 +700,8 @@
Ints :: "'a::comm_ring_1 set"
"Ints == range of_int"
-abbreviation (xsymbols)
- Ints1 ("\<int>")
- "\<int> == Ints"
+const_syntax (xsymbols)
+ Ints ("\<int>")
lemma Ints_0 [simp]: "0 \<in> Ints"
apply (simp add: Ints_def)