diff -r d276e4b53d6b -r 1f60b45c5f97 src/HOL/Complex/ex/ReflectedFerrack.thy --- 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