# HG changeset patch # User wenzelm # Date 1230841665 -3600 # Node ID 93b819a4414668590ce69f4d9a85d992e9d284fe # Parent 6cd3ac4708d248e4e1006d5a11a2afec120a615f proper import of ~~/src/HOL/ex/ReflectedFerrack; diff -r 6cd3ac4708d2 -r 93b819a44146 doc-src/IsarAdvanced/Codegen/Thy/Setup.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Thu Jan 01 21:00:33 2009 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Thu Jan 01 21:27:45 2009 +0100 @@ -5,7 +5,7 @@ ML {* no_document use_thys ["Efficient_Nat", "Code_Char_chr", "Product_ord", "Imperative_HOL", - "~~/src/HOL/Complex/ex/ReflectedFerrack"] *} + "~~/src/HOL/ex/ReflectedFerrack"] *} ML_val {* Code_Target.code_width := 74 *}