
diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Integ/NatBin.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -20,7 +20,7 @@
   nat_number_of_def: "number_of v == nat (number_of (v\<Colon>int))"
 
 abbreviation (xsymbols)
-  square :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999)
+  square :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999) where
   "x\<twosuperior> == x^2"
 
 notation (latex output)




