Admin/lib/Tools/regenerate_cooper
author paulson <lp15@cam.ac.uk>
Fri, 16 Aug 2019 12:53:36 +0100
changeset 70547 7ce95a5c4aa8
parent 70092 a19dd7006a3c
child 83008 3f3d83b9ffbc
permissions -rwxr-xr-x
new material on eqiintegrable functions, etc.

#!/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}"