# HG changeset patch
# User haftmann
# Date 1222771754 -7200
# Node ID 293b166c45c5a1ec9bb019e04fec8344b8c8a332
# Parent  f65e8b318581dc671c40ef77ffc9251706fa97d2
fixed slips

diff -r f65e8b318581 -r 293b166c45c5 doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy
--- 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
diff -r f65e8b318581 -r 293b166c45c5 doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy
--- 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:
diff -r f65e8b318581 -r 293b166c45c5 doc-src/IsarAdvanced/Codegen/Thy/ROOT.ML
--- 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";