# HG changeset patch
# User nipkow
# Date 1236945996 -3600
# Node ID b32d62c9c5835f5289015bb30a85fd03efec119b
# Parent  3e3238da8abb2626548b68536d084458f48eb740# Parent  201887dcea0a619a10077a79d76282554cb2c9ab
merged

diff -r 3e3238da8abb -r b32d62c9c583 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Fri Mar 13 12:29:38 2009 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Fri Mar 13 13:06:36 2009 +0100
@@ -92,7 +92,7 @@
       the $n$th element of @{text xs}.
 
 \item Human readers are good at converting automatically from lists to
-sets. Hence \texttt{OptionalSugar} contains syntax for supressing the
+sets. Hence \texttt{OptionalSugar} contains syntax for suppressing the
 conversion function @{const set}: for example, @{prop[source]"x \<in> set xs"}
 becomes @{prop"x \<in> set xs"}.
 
@@ -106,6 +106,17 @@
 \end{itemize}
 *}
 
+subsection{* Numbers *}
+
+text{* Coercions between numeric types are alien to mathematicians who
+consider, for example, @{typ nat} as a subset of @{typ int}.
+\texttt{OptionalSugar} contains syntax for suppressing numeric coercions such
+as @{const int} @{text"::"} @{typ"nat \<Rightarrow> int"}. For example,
+@{term[source]"int 5"} is printed as @{term "int 5"}. Embeddings of types
+@{typ nat}, @{typ int}, @{typ real} are covered; non-injective coercions such
+as @{const nat} @{text"::"} @{typ"int \<Rightarrow> nat"} are not and should not be
+hidden. *}
+
 section "Printing theorems"
 
 subsection "Question marks"
@@ -126,7 +137,7 @@
 at the beginning of your file \texttt{ROOT.ML}.
 The rest of this document is produced with this flag reset.
 
-Hint: Resetting \verb!show_question_marks! only supresses question
+Hint: Resetting \verb!show_question_marks! only suppresses question
 marks; variables that end in digits, e.g. @{text"x1"}, are still
 printed with a trailing @{text".0"}, e.g. @{text"x1.0"}, their
 internal index. This can be avoided by turning the last digit into a
diff -r 3e3238da8abb -r b32d62c9c583 doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Fri Mar 13 12:29:38 2009 +0100
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Fri Mar 13 13:06:36 2009 +0100
@@ -120,7 +120,7 @@
       the $n$th element of \isa{xs}.
 
 \item Human readers are good at converting automatically from lists to
-sets. Hence \texttt{OptionalSugar} contains syntax for supressing the
+sets. Hence \texttt{OptionalSugar} contains syntax for suppressing the
 conversion function \isa{set}: for example, \isa{{\isachardoublequote}x\ {\isasymin}\ set\ xs{\isachardoublequote}}
 becomes \isa{x\ {\isasymin}\ xs}.
 
@@ -137,6 +137,22 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsubsection{Numbers%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Coercions between numeric types are alien to mathematicians who
+consider, for example, \isa{nat} as a subset of \isa{int}.
+\texttt{OptionalSugar} contains syntax for suppressing numeric coercions such
+as \isa{int} \isa{{\isacharcolon}{\isacharcolon}} \isa{nat\ {\isasymRightarrow}\ int}. For example,
+\isa{{\isachardoublequote}int\ {\isadigit{5}}{\isachardoublequote}} is printed as \isa{{\isadigit{5}}}. Embeddings of types
+\isa{nat}, \isa{int}, \isa{real} are covered; non-injective coercions such
+as \isa{nat} \isa{{\isacharcolon}{\isacharcolon}} \isa{int\ {\isasymRightarrow}\ nat} are not and should not be
+hidden.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsection{Printing theorems%
 }
 \isamarkuptrue%
@@ -162,7 +178,7 @@
 at the beginning of your file \texttt{ROOT.ML}.
 The rest of this document is produced with this flag reset.
 
-Hint: Resetting \verb!show_question_marks! only supresses question
+Hint: Resetting \verb!show_question_marks! only suppresses question
 marks; variables that end in digits, e.g. \isa{x{\isadigit{1}}}, are still
 printed with a trailing \isa{{\isachardot}{\isadigit{0}}}, e.g. \isa{x{\isadigit{1}}{\isachardot}{\isadigit{0}}}, their
 internal index. This can be avoided by turning the last digit into a
diff -r 3e3238da8abb -r b32d62c9c583 src/HOL/Library/OptionalSugar.thy
--- a/src/HOL/Library/OptionalSugar.thy	Fri Mar 13 12:29:38 2009 +0100
+++ b/src/HOL/Library/OptionalSugar.thy	Fri Mar 13 13:06:36 2009 +0100
@@ -18,6 +18,8 @@
   "n" <= "real n"
   "n" <= "CONST real_of_nat n"
   "n" <= "CONST real_of_int n"
+  "n" <= "CONST of_real n"
+  "n" <= "CONST complex_of_real n"
 
 (* append *)
 syntax (latex output)
@@ -27,6 +29,7 @@
   "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"
 
 
+(* deprecated, use thm_style instead, will be removed *)
 (* aligning equations *)
 notation (tab output)
   "op ="  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and