src/HOL/TPTP/THF_Arith.thy

--- a/src/HOL/TPTP/THF_Arith.thy	Tue Sep 01 17:25:36 2015 +0200
+++ b/src/HOL/TPTP/THF_Arith.thy	Tue Sep 01 22:32:58 2015 +0200
@@ -16,17 +16,17 @@
 
 overloading rat_is_int \<equiv> "is_int :: rat \<Rightarrow> bool"
 begin
-  definition "rat_is_int (q\<Colon>rat) \<longleftrightarrow> (\<exists>n\<Colon>int. q = of_int n)"
+  definition "rat_is_int (q::rat) \<longleftrightarrow> (\<exists>n::int. q = of_int n)"
 end
 
 overloading real_is_int \<equiv> "is_int :: real \<Rightarrow> bool"
 begin
-  definition "real_is_int (x\<Colon>real) \<longleftrightarrow> x \<in> \<int>"
+  definition "real_is_int (x::real) \<longleftrightarrow> x \<in> \<int>"
 end
 
 overloading real_is_rat \<equiv> "is_rat :: real \<Rightarrow> bool"
 begin
-  definition "real_is_rat (x\<Colon>real) \<longleftrightarrow> x \<in> \<rat>"
+  definition "real_is_rat (x::real) \<longleftrightarrow> x \<in> \<rat>"
 end
 
 consts
@@ -36,32 +36,32 @@
 
 overloading rat_to_int \<equiv> "to_int :: rat \<Rightarrow> int"
 begin
-  definition "rat_to_int (q\<Colon>rat) = floor q"
+  definition "rat_to_int (q::rat) = floor q"
 end
 
 overloading real_to_int \<equiv> "to_int :: real \<Rightarrow> int"
 begin
-  definition "real_to_int (x\<Colon>real) = floor x"
+  definition "real_to_int (x::real) = floor x"
 end
 
 overloading int_to_rat \<equiv> "to_rat :: int \<Rightarrow> rat"
 begin
-  definition "int_to_rat (n\<Colon>int) = (of_int n\<Colon>rat)"
+  definition "int_to_rat (n::int) = (of_int n::rat)"
 end
 
 overloading real_to_rat \<equiv> "to_rat :: real \<Rightarrow> rat"
 begin
-  definition "real_to_rat (x\<Colon>real) = (inv of_rat x\<Colon>rat)"
+  definition "real_to_rat (x::real) = (inv of_rat x::rat)"
 end
 
 overloading int_to_real \<equiv> "to_real :: int \<Rightarrow> real"
 begin
-  definition "int_to_real (n\<Colon>int) = real n"
+  definition "int_to_real (n::int) = real n"
 end
 
 overloading rat_to_real \<equiv> "to_real :: rat \<Rightarrow> real"
 begin
-  definition "rat_to_real (x\<Colon>rat) = (of_rat x\<Colon>real)"
+  definition "rat_to_real (x::rat) = (of_rat x::real)"
 end
 
 declare
@@ -75,16 +75,16 @@
   int_to_real_def [simp]
   rat_to_real_def [simp]
 
-lemma to_rat_is_int [intro, simp]: "is_int (to_rat (n\<Colon>int))"
+lemma to_rat_is_int [intro, simp]: "is_int (to_rat (n::int))"
 by (metis int_to_rat_def rat_is_int_def)
 
-lemma to_real_is_int [intro, simp]: "is_int (to_real (n\<Colon>int))"
+lemma to_real_is_int [intro, simp]: "is_int (to_real (n::int))"
 by (metis Ints_real_of_int int_to_real_def real_is_int_def)
 
-lemma to_real_is_rat [intro, simp]: "is_rat (to_real (q\<Colon>rat))"
+lemma to_real_is_rat [intro, simp]: "is_rat (to_real (q::rat))"
 by (metis Rats_of_rat rat_to_real_def real_is_rat_def)
 
-lemma inj_of_rat [intro, simp]: "inj (of_rat\<Colon>rat\<Rightarrow>real)"
+lemma inj_of_rat [intro, simp]: "inj (of_rat::rat\<Rightarrow>real)"
 by (metis injI of_rat_eq_iff)
 
 end