src/HOL/Complex/ex/ReflectedFerrack.thy
changeset 24249 1f60b45c5f97
parent 23854 688a8a7bcd4e
child 24336 fff40259f336
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Mon Aug 13 21:22:37 2007 +0200
@@ -1993,7 +1993,7 @@
   "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
     (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
 
-code_gen linrqe ferrack_test in SML to Ferrack
+code_gen linrqe ferrack_test in SML module_name Ferrack
 
 (*code_module Ferrack
   contains