--- a/doc-src/Codegen/Thy/Adaptation.thy Thu Jul 15 08:14:05 2010 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy Thu Jul 15 10:16:17 2010 +0200
@@ -220,12 +220,12 @@
infix ``@{verbatim "*"}'' type constructor and parentheses:
*}
(*<*)
-code_type %invisible *
+code_type %invisible prod
(SML)
code_const %invisible Pair
(SML)
(*>*)
-code_type %quotett *
+code_type %quotett prod
(SML infix 2 "*")
code_const %quotett Pair
(SML "!((_),/ (_))")
--- a/doc-src/Codegen/Thy/Further.thy Thu Jul 15 08:14:05 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy Thu Jul 15 10:16:17 2010 +0200
@@ -62,7 +62,7 @@
term @{term [source] "power.powers (\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"}
(see \cite{isabelle-locale} for the details behind).
- Furtunately, with minor effort the desired behaviour can be achieved.
+ Fortunately, with minor effort the desired behaviour can be achieved.
First, a dedicated definition of the constant on which the local @{text "powers"}
after interpretation is supposed to be mapped on:
*}
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Thu Jul 15 08:14:05 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Thu Jul 15 10:16:17 2010 +0200
@@ -455,7 +455,7 @@
%
\isatagquotett
\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
-\ {\isacharasterisk}\isanewline
+\ prod\isanewline
\ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
\ Pair\isanewline
--- a/doc-src/Codegen/Thy/document/Further.tex Thu Jul 15 08:14:05 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex Thu Jul 15 10:16:17 2010 +0200
@@ -115,7 +115,7 @@
term \isa{{\isachardoublequote}power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequote}}
(see \cite{isabelle-locale} for the details behind).
- Furtunately, with minor effort the desired behaviour can be achieved.
+ Fortunately, with minor effort the desired behaviour can be achieved.
First, a dedicated definition of the constant on which the local \isa{powers}
after interpretation is supposed to be mapped on:%
\end{isamarkuptext}%