# HG changeset patch
# User huffman
# Date 1333716000 -7200
# Node ID a0f257197741840418f0de5b54195de9ad69692d
# Parent  09c5160ba550a15d07ff80f86ccdc388ceacbbc5
remove now-unnecessary type annotations from lift_definition commands

diff -r 09c5160ba550 -r a0f257197741 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Apr 06 14:39:27 2012 +0200
+++ b/src/HOL/Word/Word.thy	Fri Apr 06 14:40:00 2012 +0200
@@ -272,33 +272,29 @@
 
 subsection  "Arithmetic operations"
 
-lift_definition word_succ :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x::int. x + 1"
+lift_definition word_succ :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x + 1"
   by (metis bintr_ariths(6))
 
-lift_definition word_pred :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x::int. x - 1"
+lift_definition word_pred :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x - 1"
   by (metis bintr_ariths(7))
 
 instantiation word :: (len0) "{neg_numeral, Divides.div, comm_monoid_mult, comm_ring}"
 begin
 
-lift_definition zero_word :: "'a word" is "0::int" .
-
-lift_definition one_word :: "'a word" is "1::int" .
-
-lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is "op + :: int \<Rightarrow> int \<Rightarrow> int"
+lift_definition zero_word :: "'a word" is "0" .
+
+lift_definition one_word :: "'a word" is "1" .
+
+lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op +"
   by (metis bintr_ariths(2))
 
-lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is "op - :: int \<Rightarrow> int \<Rightarrow> int"
+lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op -"
   by (metis bintr_ariths(3))
 
-lift_definition uminus_word :: "'a word \<Rightarrow> 'a word"
-  is "uminus :: int \<Rightarrow> int"
+lift_definition uminus_word :: "'a word \<Rightarrow> 'a word" is uminus
   by (metis bintr_ariths(5))
 
-lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is "op * :: int \<Rightarrow> int \<Rightarrow> int"
+lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op *"
   by (metis bintr_ariths(4))
 
 definition
@@ -394,20 +390,16 @@
 instantiation word :: (len0) bits
 begin
 
-lift_definition bitNOT_word :: "'a word \<Rightarrow> 'a word"
-  is "bitNOT :: int \<Rightarrow> int"
+lift_definition bitNOT_word :: "'a word \<Rightarrow> 'a word" is bitNOT
   by (metis bin_trunc_not)
 
-lift_definition bitAND_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is "bitAND :: int \<Rightarrow> int \<Rightarrow> int"
+lift_definition bitAND_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is bitAND
   by (metis bin_trunc_and)
 
-lift_definition bitOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is "bitOR :: int \<Rightarrow> int \<Rightarrow> int"
+lift_definition bitOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is bitOR
   by (metis bin_trunc_or)
 
-lift_definition bitXOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is "bitXOR :: int \<Rightarrow> int \<Rightarrow> int"
+lift_definition bitXOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is bitXOR
   by (metis bin_trunc_xor)
 
 definition