src/HOL/Int.thy
 changeset 61070 b72a990adfe2 parent 60868 dd18c33c001e child 61076 bdc1e2f0a86a
```     1.1 --- a/src/HOL/Int.thy	Mon Aug 31 21:01:21 2015 +0200
1.2 +++ b/src/HOL/Int.thy	Mon Aug 31 21:28:08 2015 +0200
1.3 @@ -623,11 +623,8 @@
1.4  context ring_1
1.5  begin
1.6
1.7 -definition Ints  :: "'a set" where
1.8 -  "Ints = range of_int"
1.9 -
1.10 -notation (xsymbols)
1.11 -  Ints  ("\<int>")
1.12 +definition Ints :: "'a set"  ("\<int>")
1.13 +  where "\<int> = range of_int"
1.14
1.15  lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
1.17 @@ -687,7 +684,7 @@
1.18  text \<open>The premise involving @{term Ints} prevents @{term "a = 1/2"}.\<close>
1.19
1.20  lemma Ints_double_eq_0_iff:
1.21 -  assumes in_Ints: "a \<in> Ints"
1.22 +  assumes in_Ints: "a \<in> \<int>"
1.23    shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
1.24  proof -
1.25    from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
1.26 @@ -706,7 +703,7 @@
1.27  qed
1.28
1.29  lemma Ints_odd_nonzero:
1.30 -  assumes in_Ints: "a \<in> Ints"
1.31 +  assumes in_Ints: "a \<in> \<int>"
1.32    shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
1.33  proof -
1.34    from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
1.35 @@ -720,11 +717,11 @@
1.36    qed
1.37  qed
1.38
1.39 -lemma Nats_numeral [simp]: "numeral w \<in> Nats"
1.40 +lemma Nats_numeral [simp]: "numeral w \<in> \<nat>"
1.41    using of_nat_in_Nats [of "numeral w"] by simp
1.42
1.43  lemma Ints_odd_less_0:
1.44 -  assumes in_Ints: "a \<in> Ints"
1.45 +  assumes in_Ints: "a \<in> \<int>"
1.46    shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
1.47  proof -
1.48    from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
```