| author | wenzelm |
| Sun, 10 Nov 2024 13:40:28 +0100 | |
| changeset 81422 | b6928aa389f7 |
| 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}"
|