# HG changeset patch
# User haftmann
# Date 1232115550 -3600
# Node ID fc20414d4aa8bea5e20e71c4b3eb7b5d95c3c4f4
# Parent  363f17dee9cad7cf9c34d80dbbbafc3f01e71393
fixed location of Imperative_HOL

diff -r 363f17dee9ca -r fc20414d4aa8 doc-src/IsarAdvanced/Codegen/Thy/Setup.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy	Fri Jan 16 15:14:16 2009 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy	Fri Jan 16 15:19:10 2009 +0100
@@ -4,7 +4,7 @@
 begin
 
 ML {* no_document use_thys
-  ["Efficient_Nat", "Code_Char_chr", "Product_ord", "Imperative_HOL",
+  ["Efficient_Nat", "Code_Char_chr", "Product_ord", "~~/src/HOL/Imperative_HOL/Imperative_HOL",
    "~~/src/HOL/ex/ReflectedFerrack"] *}
 
 ML_val {* Code_Target.code_width := 74 *}