prefer concise "isabelle process_theories", which only uses the required theories;
authorwenzelm
Sat, 16 Aug 2025 13:06:26 +0200
changeset 83008 3f3d83b9ffbc
parent 83007 b9715600883c
child 83010 b01548bf9e77
child 83012 fb5310760fce
prefer concise "isabelle process_theories", which only uses the required theories;
Admin/lib/Tools/regenerate_cooper
--- a/Admin/lib/Tools/regenerate_cooper	Sat Aug 16 12:50:32 2025 +0200
+++ b/Admin/lib/Tools/regenerate_cooper	Sat Aug 16 13:06:26 2025 +0200
@@ -2,11 +2,8 @@
 #
 # Author: Florian Haftmann, TU Muenchen
 #
-# DESCRIPTION: regenerate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML from ~~/src/HOL/Decision_Proc/Cooper.thy
+# DESCRIPTION: regenerate ~~/src/HOL/Tools/Qelim/cooper_procedure.ML from theory HOL-Decision_Procs.Cooper
 
-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}"
+isabelle process_theories \
+  -E '(in "~~/src/HOL/Tools/Qelim") [2] "HOL-Decision_Procs.Cooper:code/cooper_procedure.ML"' \
+  HOL-Decision_Procs.Cooper