author | haftmann |
Fri, 30 Apr 2010 18:34:51 +0200 | |
changeset 36608 | 16736dde54c0 |
parent 36578 | 663bb2bc1e72 |
child 36609 | 6ed6112f0a95 |
--- a/src/HOL/Decision_Procs/Cooper.thy Fri Apr 30 17:53:49 2010 +0200 +++ b/src/HOL/Decision_Procs/Cooper.thy Fri Apr 30 18:34:51 2010 +0200 @@ -1909,9 +1909,11 @@ ML {* @{code cooper_test} () *} +(* code_reflect Generated_Cooper functions pa file "~~/src/HOL/Tools/Qelim/generated_cooper.ML" +*) oracle linzqe_oracle = {* let