author | haftmann |
Mon, 03 May 2010 07:59:51 +0200 | |
changeset 36609 | 6ed6112f0a95 |
parent 36607 | e5f7235f39c5 (current diff) |
parent 36608 | 16736dde54c0 (diff) |
child 36610 | bafd82950e24 |
child 36622 | e393a91f86df |
--- a/src/HOL/Decision_Procs/Cooper.thy Sat May 01 21:29:03 2010 +0200 +++ b/src/HOL/Decision_Procs/Cooper.thy Mon May 03 07:59: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