author | kleing |
Tue, 08 Apr 2008 09:42:18 +0200 | |
changeset 26573 | ea36563210cc |
parent 26572 | 9178a7f4c4c8 |
child 26574 | 560d07845442 |
--- 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