--- a/doc-src/Codegen/Thy/Adaptation.thy Wed Nov 03 14:14:05 2010 +0100
+++ b/doc-src/Codegen/Thy/Adaptation.thy Wed Nov 03 14:14:05 2010 +0100
@@ -2,7 +2,8 @@
imports Setup
begin
-setup %invisible {* Code_Target.extend_target ("\<SML>", ("SML", K I)) *}
+setup %invisible {* Code_Target.extend_target ("\<SML>", ("SML", K I))
+ #> Code_Target.extend_target ("\<SMLdummy>", ("Haskell", K I)) *}
section {* Adaptation to target languages \label{sec:adaptation} *}
@@ -235,7 +236,7 @@
@{command_def "code_reserved"} command:
*}
-code_reserved %quote "\<SML>" bool true false andalso
+code_reserved %quote "\<SMLdummy>" bool true false andalso
text {*
\noindent Next, we try to map HOL pairs to SML pairs, using the
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Wed Nov 03 14:14:05 2010 +0100
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Wed Nov 03 14:14:05 2010 +0100
@@ -26,7 +26,8 @@
%
\isataginvisible
\isacommand{setup}\isamarkupfalse%
-\ {\isacharverbatimopen}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSML}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}SML{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%
+\ {\isacharverbatimopen}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSML}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}SML{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\isanewline
+\ \ {\isacharhash}{\isachargreater}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSMLdummy}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}Haskell{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%
\endisataginvisible
{\isafoldinvisible}%
%
@@ -420,7 +421,7 @@
%
\isatagquote
\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymSML}{\isachardoublequoteclose}\ bool\ true\ false\ andalso%
+\ {\isachardoublequoteopen}{\isasymSMLdummy}{\isachardoublequoteclose}\ bool\ true\ false\ andalso%
\endisatagquote
{\isafoldquote}%
%
--- a/doc-src/Codegen/style.sty Wed Nov 03 14:14:05 2010 +0100
+++ b/doc-src/Codegen/style.sty Wed Nov 03 14:14:05 2010 +0100
@@ -45,6 +45,7 @@
%% a trick
\newcommand{\isasymSML}{SML}
+\newcommand{\isasymSMLdummy}{SML}
%% presentation
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}