--- a/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy Tue Sep 30 11:19:47 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy Tue Sep 30 12:49:14 2008 +0200
@@ -106,8 +106,6 @@
text %quoteme {*@{code_stmts in_interval (SML)}*}
text {*
- \lstsml{Thy/examples/bool_mlbool.ML}
-
\noindent This still is not perfect: the parentheses
around the \qt{andalso} expression are superfluous.
Though the serializer
--- a/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy Tue Sep 30 11:19:47 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy Tue Sep 30 12:49:14 2008 +0200
@@ -97,7 +97,7 @@
(with extension @{text ".hs"}) is written:
*}
-export_code %quoteme empty dequeue enqueue in SML module_name Example file "examples/Example.ML"
+export_code %quoteme empty dequeue enqueue in Haskell module_name Example file "examples/"
text {*
\noindent This is how the corresponding code in @{text Haskell} looks like:
--- a/doc-src/IsarAdvanced/Codegen/Thy/ROOT.ML Tue Sep 30 11:19:47 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/ROOT.ML Tue Sep 30 12:49:14 2008 +0200
@@ -2,7 +2,7 @@
(* $Id$ *)
no_document use_thy "Setup";
-no_document use_thys ["Efficient_Nat", "Code_Integer"];
+no_document use_thys ["Efficient_Nat"];
use_thy "Introduction";
use_thy "Program";