# HG changeset patch
# User haftmann
# Date 1279181777 -7200
# Node ID 6e17a56514cefe103d870ecc3a538ec986e9955e
# Parent  d8fdbcbde4b61e192de1e29f089bae799369e34a# Parent  2bcce92be29129c2f4ee4ae01d8733fd3cf32576
merged

diff -r d8fdbcbde4b6 -r 6e17a56514ce doc-src/Codegen/Thy/Adaptation.thy
--- 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 "!((_),/ (_))")
diff -r d8fdbcbde4b6 -r 6e17a56514ce doc-src/Codegen/Thy/Further.thy
--- 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:
 *}
diff -r d8fdbcbde4b6 -r 6e17a56514ce doc-src/Codegen/Thy/document/Adaptation.tex
--- 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
diff -r d8fdbcbde4b6 -r 6e17a56514ce doc-src/Codegen/Thy/document/Further.tex
--- 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}%