author | haftmann |
Fri, 29 Jun 2007 16:05:00 +0200 | |
changeset 23518 | 6407d832da03 |
parent 23517 | 93d1ad7662a9 |
child 23519 | a4ffa756d8eb |
--- 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"