removed abbrev for word_power. Was in the wrong direction and unused.
authorkleing
Tue, 08 Apr 2008 09:42:18 +0200
changeset 26573 ea36563210cc
parent 26572 9178a7f4c4c8
child 26574 560d07845442
removed abbrev for word_power. Was in the wrong direction and unused.
src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Mon Apr 07 21:29:46 2008 +0200
+++ b/src/HOL/Word/WordDefinition.thy	Tue Apr 08 09:42:18 2008 +0200
@@ -162,11 +162,6 @@
 
 end 
 
-abbreviation
-  word_power :: "'a\<Colon>len0 word \<Rightarrow> nat \<Rightarrow> 'a word"
-where
-  "word_power == op ^"
-
 definition
   word_succ :: "'a :: len0 word => 'a word"
 where