author | haftmann |
Wed, 14 Sep 2011 23:47:04 +0200 | |
changeset 44931 | 74b6ead3c365 |
parent 44930 | afcbf23508af |
child 44933 | 9795fdc87965 |
--- a/src/HOL/Decision_Procs/Cooper.thy Wed Sep 14 23:46:02 2011 +0200 +++ b/src/HOL/Decision_Procs/Cooper.thy Wed Sep 14 23:47:04 2011 +0200 @@ -1871,11 +1871,9 @@ ML {* @{code cooper_test} () *} -(* -code_reflect Cooper_Procedure +(* code_reflect Cooper_Procedure functions pa - file "~~/src/HOL/Tools/Qelim/generated_cooper.ML" -*) + file "~~/src/HOL/Tools/Qelim/cooper_procedure.ML" *) oracle linzqe_oracle = {* let