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.16    by (simp add: Ints_def)
    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] .