src/HOL/Int.thy
changeset 61076 bdc1e2f0a86a
parent 61070 b72a990adfe2
child 61144 5e94dfead1c2
     1.1 --- a/src/HOL/Int.thy	Tue Sep 01 17:25:36 2015 +0200
     1.2 +++ b/src/HOL/Int.thy	Tue Sep 01 22:32:58 2015 +0200
     1.3 @@ -107,10 +107,10 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
     1.8 +  "(inf :: int \<Rightarrow> int \<Rightarrow> int) = min"
     1.9  
    1.10  definition
    1.11 -  "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
    1.12 +  "(sup :: int \<Rightarrow> int \<Rightarrow> int) = max"
    1.13  
    1.14  instance
    1.15    by intro_classes
    1.16 @@ -161,10 +161,10 @@
    1.17  begin
    1.18  
    1.19  definition
    1.20 -  zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
    1.21 +  zabs_def: "\<bar>i::int\<bar> = (if i < 0 then - i else i)"
    1.22  
    1.23  definition
    1.24 -  zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
    1.25 +  zsgn_def: "sgn (i::int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
    1.26  
    1.27  instance proof
    1.28    fix i j k :: int
    1.29 @@ -172,17 +172,17 @@
    1.30      by (rule zmult_zless_mono2)
    1.31    show "\<bar>i\<bar> = (if i < 0 then -i else i)"
    1.32      by (simp only: zabs_def)
    1.33 -  show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
    1.34 +  show "sgn (i::int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
    1.35      by (simp only: zsgn_def)
    1.36  qed
    1.37  
    1.38  end
    1.39  
    1.40 -lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
    1.41 +lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1::int) \<le> z"
    1.42    by transfer clarsimp
    1.43  
    1.44  lemma zless_iff_Suc_zadd:
    1.45 -  "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))"
    1.46 +  "(w :: int) < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))"
    1.47  apply transfer
    1.48  apply auto
    1.49  apply (rename_tac a b c d)
    1.50 @@ -438,7 +438,7 @@
    1.51  
    1.52  subsection\<open>Lemmas about the Function @{term of_nat} and Orderings\<close>
    1.53  
    1.54 -lemma negative_zless_0: "- (int (Suc n)) < (0 \<Colon> int)"
    1.55 +lemma negative_zless_0: "- (int (Suc n)) < (0 :: int)"
    1.56  by (simp add: order_less_le del: of_nat_Suc)
    1.57  
    1.58  lemma negative_zless [iff]: "- (int (Suc n)) < int m"
    1.59 @@ -1117,9 +1117,9 @@
    1.60  lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
    1.61  proof
    1.62    assume "finite (UNIV::int set)"
    1.63 -  moreover have "inj (\<lambda>i\<Colon>int. 2 * i)"
    1.64 +  moreover have "inj (\<lambda>i::int. 2 * i)"
    1.65      by (rule injI) simp
    1.66 -  ultimately have "surj (\<lambda>i\<Colon>int. 2 * i)"
    1.67 +  ultimately have "surj (\<lambda>i::int. 2 * i)"
    1.68      by (rule finite_UNIV_inj_surj)
    1.69    then obtain i :: int where "1 = 2 * i" by (rule surjE)
    1.70    then show False by (simp add: pos_zmult_eq_1_iff)