--- 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
--- 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
--- 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