--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/lib/Tools/regenerate_cooper Tue Apr 09 16:59:00 2019 +0000
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+#
+# Author: Florian Haftmann, TU Muenchen
+#
+# DESCRIPTION: regenerate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML from ~~/src/HOL/Decision_Proc/Cooper.thy
+
+session=HOL-Decision_Procs
+src='HOL-Decision_Procs.Cooper:code/cooper_procedure.ML'
+dst='~~/src/HOL/Tools/Qelim/'
+
+"${ISABELLE_TOOL}" build "${session}"
+"${ISABELLE_TOOL}" export -x "${src}" -p 2 -O "${dst}" "${session}"
--- a/src/HOL/Decision_Procs/Cooper.thy Tue Apr 09 16:59:00 2019 +0000
+++ b/src/HOL/Decision_Procs/Cooper.thy Tue Apr 09 16:59:00 2019 +0000
@@ -2663,8 +2663,7 @@
subsection \<open>Variant for HOL-Main\<close>
--(*code_reflect Cooper_Procedure
-- functions pa T Bound nat_of_integer integer_of_nat int_of_integer integer_of_int
-- file "~~/src/HOL/Tools/Qelim/cooper_procedure.ML"*)
+export_code pa T Bound nat_of_integer integer_of_nat int_of_integer integer_of_int
+ in Eval module_name Cooper_Procedure file_prefix cooper_procedure
end