| author | wenzelm |
| Mon, 03 Mar 2025 19:52:18 +0100 | |
| changeset 82231 | cbe937aa5e90 |
| parent 70092 | a19dd7006a3c |
| child 83008 | 3f3d83b9ffbc |
| permissions | -rwxr-xr-x |
|
70092
a19dd7006a3c
more explicit way to re-generate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML
haftmann
parents:
diff
changeset
|
1 |
#!/usr/bin/env bash |
|
a19dd7006a3c
more explicit way to re-generate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML
haftmann
parents:
diff
changeset
|
2 |
# |
|
a19dd7006a3c
more explicit way to re-generate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML
haftmann
parents:
diff
changeset
|
3 |
# Author: Florian Haftmann, TU Muenchen |
|
a19dd7006a3c
more explicit way to re-generate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML
haftmann
parents:
diff
changeset
|
4 |
# |
|
a19dd7006a3c
more explicit way to re-generate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML
haftmann
parents:
diff
changeset
|
5 |
# DESCRIPTION: regenerate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML from ~~/src/HOL/Decision_Proc/Cooper.thy |
|
a19dd7006a3c
more explicit way to re-generate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML
haftmann
parents:
diff
changeset
|
6 |
|
|
a19dd7006a3c
more explicit way to re-generate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML
haftmann
parents:
diff
changeset
|
7 |
session=HOL-Decision_Procs |
|
a19dd7006a3c
more explicit way to re-generate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML
haftmann
parents:
diff
changeset
|
8 |
src='HOL-Decision_Procs.Cooper:code/cooper_procedure.ML' |
|
a19dd7006a3c
more explicit way to re-generate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML
haftmann
parents:
diff
changeset
|
9 |
dst='~~/src/HOL/Tools/Qelim/' |
|
a19dd7006a3c
more explicit way to re-generate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML
haftmann
parents:
diff
changeset
|
10 |
|
|
a19dd7006a3c
more explicit way to re-generate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML
haftmann
parents:
diff
changeset
|
11 |
"${ISABELLE_TOOL}" build "${session}"
|
|
a19dd7006a3c
more explicit way to re-generate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML
haftmann
parents:
diff
changeset
|
12 |
"${ISABELLE_TOOL}" export -x "${src}" -p 2 -O "${dst}" "${session}"
|