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