| 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