avoid inclusion of Natural module in generated code
authorhaftmann
Wed, 11 Aug 2010 11:52:40 +0200
changeset 38322 5888841c38da
parent 38321 7edf0ab9d5cb
child 38323 dc2a61b98bab
avoid inclusion of Natural module in generated code
doc-src/Classes/Thy/Classes.thy
doc-src/Classes/Thy/document/Classes.tex
--- a/doc-src/Classes/Thy/Classes.thy	Wed Aug 11 09:06:31 2010 +0200
+++ b/doc-src/Classes/Thy/Classes.thy	Wed Aug 11 11:52:40 2010 +0200
@@ -611,13 +611,12 @@
 text {*
   \noindent This maps to Haskell as follows:
 *}
-
+(*<*)code_include %invisible Haskell "Natural" -(*>*)
 text %quote {*@{code_stmts example (Haskell)}*}
 
 text {*
   \noindent The code in SML has explicit dictionary passing:
 *}
-
 text %quote {*@{code_stmts example (SML)}*}
 
 subsection {* Inspecting the type class universe *}
--- a/doc-src/Classes/Thy/document/Classes.tex	Wed Aug 11 09:06:31 2010 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex	Wed Aug 11 11:52:40 2010 +0200
@@ -1132,6 +1132,19 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isataginvisible
+%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
 \isadelimquote
 %
 \endisadelimquote