| author | desharna |
| Thu, 02 Oct 2025 11:02:15 +0000 | |
| changeset 83240 | dfa14d921fd2 |
| parent 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 |
# |
|
83008
3f3d83b9ffbc
prefer concise "isabelle process_theories", which only uses the required theories;
wenzelm
parents:
70092
diff
changeset
|
5 |
# DESCRIPTION: regenerate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML from theory HOL-Decision_Procs.Cooper |
|
70092
a19dd7006a3c
more explicit way to re-generate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML
haftmann
parents:
diff
changeset
|
6 |
|
|
83008
3f3d83b9ffbc
prefer concise "isabelle process_theories", which only uses the required theories;
wenzelm
parents:
70092
diff
changeset
|
7 |
isabelle process_theories \ |
|
3f3d83b9ffbc
prefer concise "isabelle process_theories", which only uses the required theories;
wenzelm
parents:
70092
diff
changeset
|
8 |
-E '(in "~~/src/HOL/Tools/Qelim") [2] "HOL-Decision_Procs.Cooper:code/cooper_procedure.ML"' \ |
|
3f3d83b9ffbc
prefer concise "isabelle process_theories", which only uses the required theories;
wenzelm
parents:
70092
diff
changeset
|
9 |
HOL-Decision_Procs.Cooper |