| changeset 23518 | 6407d832da03 |
| parent 23515 | 3e7f62e68fe4 |
| child 23810 | f5e6932d0500 |
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy Thu Jun 28 19:09:43 2007 +0200 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Fri Jun 29 16:05:00 2007 +0200 @@ -2004,7 +2004,6 @@ ML {* Ferrack.ReflectedFerrack.ferrack_test () *} -code_gen linrqe ferrack_test in SML file "~~/../../gen_code/ferrack.ML" use "linreif.ML" oracle linr_oracle ("term") = ReflectedFerrack.linrqe_oracle use"linrtac.ML"