--- a/doc-src/Codegen/Thy/Setup.thy Thu Sep 02 16:41:42 2010 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy Thu Sep 02 16:41:44 2010 +0200
@@ -1,15 +1,12 @@
theory Setup
-imports Complex_Main More_List RBT Dlist Mapping
+imports
+ Complex_Main
+ More_List RBT Dlist Mapping
uses
"../../antiquote_setup.ML"
"../../more_antiquote.ML"
begin
-ML {* no_document use_thys
- ["Efficient_Nat", "Code_Char_chr", "Product_ord",
- "~~/src/HOL/Imperative_HOL/Imperative_HOL",
- "~~/src/HOL/Decision_Procs/Ferrack"] *}
-
setup {*
let
val typ = Simple_Syntax.read_typ;