fixed location of Imperative_HOL
authorhaftmann
Fri, 16 Jan 2009 15:19:10 +0100
changeset 29514 fc20414d4aa8
parent 29513 363f17dee9ca
child 29518 c3b9c0d24fec
child 29523 f83dcdcee6b3
fixed location of Imperative_HOL
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 *}