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}"