| changeset 21404 | eb85850d3eb7 |
| parent 21210 | c17fd2df4e9e |
| child 22046 | ce84c9887e2d |
--- 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)