--- a/NEWS Sun May 04 21:02:54 2025 +0100
+++ b/NEWS Sun May 04 21:03:04 2025 +0100
@@ -59,6 +59,12 @@
not available as SVG.
+*** Pure ***
+
+* Command 'thy_deps' expects optional theory arguments as long theory names,
+the same way as the 'imports' clause. Minor INCOMPATIBILITY.
+
+
*** HOL ***
* Normalization by evaluation (method "normalization", command value) could
--- a/src/HOL/List.thy Sun May 04 21:02:54 2025 +0100
+++ b/src/HOL/List.thy Sun May 04 21:03:04 2025 +0100
@@ -2440,6 +2440,19 @@
lemma nth_image: "l \<le> size xs \<Longrightarrow> nth xs ` {0..<l} = set(take l xs)"
by (simp add: set_conv_nth) force
+lemma set_list_update:
+ "set (xs [i := k]) = insert k (set (take i xs) \<union> set (drop (Suc i) xs))"
+ if \<open>i < length xs\<close>
+using that proof (induct xs arbitrary: i)
+ case Nil
+ then show ?case
+ by simp
+next
+ case (Cons x xs i)
+ then show ?case
+ by (cases i) (simp_all add: insert_commute)
+qed
+
subsubsection \<open>\<^const>\<open>takeWhile\<close> and \<^const>\<open>dropWhile\<close>\<close>
--- a/src/Pure/Tools/thy_deps.ML Sun May 04 21:02:54 2025 +0100
+++ b/src/Pure/Tools/thy_deps.ML Sun May 04 21:03:04 2025 +0100
@@ -36,6 +36,6 @@
let val thy0 = Proof_Context.theory_of ctxt
in if Context.subthy (thy, thy0) then thy else raise THEORY ("Bad theory", [thy, thy0]) end);
-val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps (Theory.check {long = false});
+val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps (Theory.check {long = true});
end;