merged
authorpaulson
Sun, 04 May 2025 21:03:04 +0100
changeset 82601 43f4f9c5c6bd
parent 82599 98571d7e4a7d (diff)
parent 82600 f62666eea755 (current diff)
child 82602 700f9b01c9d9
child 82603 5648293625a5
merged
--- 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;