# HG changeset patch
# User haftmann
# Date 1554829140 0
# Node ID a19dd7006a3c69c423705ad03e3e570f55a96394
# Parent  70841633b3e181302fdd8e2084530eae39f458d8
more explicit way to re-generate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML

diff -r 70841633b3e1 -r a19dd7006a3c Admin/lib/Tools/regenerate_cooper
--- /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}"
diff -r 70841633b3e1 -r a19dd7006a3c src/HOL/Decision_Procs/Cooper.thy
--- 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