# HG changeset patch
# User wenzelm
# Date 1755342386 -7200
# Node ID 3f3d83b9ffbc6d3298b737593c9c077149e3aabd
# Parent  b9715600883c4269f03680b1b36120aa16247290
prefer concise "isabelle process_theories", which only uses the required theories;

diff -r b9715600883c -r 3f3d83b9ffbc 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