src/HOL/Int.thy

--- a/src/HOL/Int.thy	Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/Int.thy	Wed May 15 12:10:39 2013 +0200
@@ -37,11 +37,9 @@
 instantiation int :: comm_ring_1
 begin
 
-lift_definition zero_int :: "int" is "(0, 0)"
-  by simp
+lift_definition zero_int :: "int" is "(0, 0)" .
 
-lift_definition one_int :: "int" is "(1, 0)"
-  by simp
+lift_definition one_int :: "int" is "(1, 0)" .
 
 lift_definition plus_int :: "int \<Rightarrow> int \<Rightarrow> int"
   is "\<lambda>(x, y) (u, v). (x + u, y + v)"