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