src/HOL/Int.thy

 subsection \<open>The Set of Integers\<close>
 
 context ring_1
 begin
 
-definition Ints  :: "'a set" where
-  "Ints = range of_int"
-
-notation (xsymbols)
-  Ints  ("\<int>")
+definition Ints :: "'a set"  ("\<int>")
+  where "\<int> = range of_int"
 
 lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
   by (simp add: Ints_def)
 
 lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>"

 end
 
 text \<open>The premise involving @{term Ints} prevents @{term "a = 1/2"}.\<close>
 
 lemma Ints_double_eq_0_iff:
-  assumes in_Ints: "a \<in> Ints"
+  assumes in_Ints: "a \<in> \<int>"
   shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
 proof -
   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
   then obtain z where a: "a = of_int z" ..
   show ?thesis

     thus "a = 0" by (simp add: a)
   qed
 qed
 
 lemma Ints_odd_nonzero:
-  assumes in_Ints: "a \<in> Ints"
+  assumes in_Ints: "a \<in> \<int>"
   shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
 proof -
   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
   then obtain z where a: "a = of_int z" ..
   show ?thesis

     hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
     with odd_nonzero show False by blast
   qed
 qed
 
-lemma Nats_numeral [simp]: "numeral w \<in> Nats"
+lemma Nats_numeral [simp]: "numeral w \<in> \<nat>"
   using of_nat_in_Nats [of "numeral w"] by simp
 
 lemma Ints_odd_less_0:
-  assumes in_Ints: "a \<in> Ints"
+  assumes in_Ints: "a \<in> \<int>"
   shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
 proof -
   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
   then obtain z where a: "a = of_int z" ..
   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"