# HG changeset patch
# User wenzelm
# Date 1010952839 -3600
# Node ID 9d80e3746eb0d1e6b8e6664098cf1bd6f70eca0d
# Parent  b0b012b11a36e3b39b3237216a0f4b38b38816a7
symbolic syntax for x^2 (faills back on plain infix "^");

diff -r b0b012b11a36 -r 9d80e3746eb0 src/HOL/Numeral.thy
--- a/src/HOL/Numeral.thy	Sun Jan 13 21:13:27 2002 +0100
+++ b/src/HOL/Numeral.thy	Sun Jan 13 21:13:59 2002 +0100
@@ -31,9 +31,19 @@
 
 setup NumeralSyntax.setup
 
+syntax (xsymbols)
+  "_square" :: "'a => 'a"  ("(_\<twosuperior>)" [1000] 999)
+syntax (HTML output)
+  "_square" :: "'a => 'a"  ("(_\<twosuperior>)" [1000] 999)
+syntax (output)
+  "_square" :: "'a => 'a"  ("(_ ^/ 2)" [81] 80)
+translations
+  "x\<twosuperior>" == "x^2"
+  "x\<twosuperior>" <= "x^(2::nat)"
 
-(*Unfold all "let"s involving constants*)
+
 lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
+  -- {* Unfold all @{text let}s involving constants *}
   by (simp add: Let_def)
 
 lemma Let_0 [simp]: "Let 0 f == f 0"