# HG changeset patch
# User wenzelm
# Date 1727384641 -7200
# Node ID 980cc422526ecd7ca7cc24049b6178cee8bb10f7
# Parent  97924a26a5c3e80da3f7c17f9bf13239dc558363# Parent  cf96b584724df6ff1fa0a2d9b1d13512c8f56db9
merged

diff -r cf96b584724d -r 980cc422526e src/HOL/Complex_Analysis/Laurent_Convergence.thy
--- a/src/HOL/Complex_Analysis/Laurent_Convergence.thy	Thu Sep 26 21:55:46 2024 +0200
+++ b/src/HOL/Complex_Analysis/Laurent_Convergence.thy	Thu Sep 26 23:04:01 2024 +0200
@@ -598,7 +598,7 @@
     by (rule asymp_equiv_symI, rule has_laurent_expansion_imp_asymp_equiv_0) fact
   show "(\<lambda>z. fls_nth F (fls_subdegree F) * z powi fls_subdegree F) \<midarrow>0\<rightarrow> fls_nth F 0"
     by (rule tendsto_eq_intros refl | use assms(2) in simp)+
-       (use assms(2) in \<open>auto simp: power_int_0_left_If\<close>)
+       (use assms(2) in \<open>auto simp: power_int_0_left_if\<close>)
 qed
 
 lemma has_laurent_expansion_imp_tendsto:
diff -r cf96b584724d -r 980cc422526e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Sep 26 21:55:46 2024 +0200
+++ b/src/HOL/HOL.thy	Thu Sep 26 23:04:01 2024 +0200
@@ -633,6 +633,11 @@
   shows R
   using assms by (elim impCE)
 
+text \<open>The analogous introduction rule for conjunction, above, is even constructive\<close>
+lemma context_disjE:
+  assumes major: "P \<or> Q" and minor: "P \<Longrightarrow> R" "\<not>P \<Longrightarrow> Q \<Longrightarrow> R"
+  shows R
+  by (iprover intro: disjE [OF major] disjE [OF excluded_middle] assms)
 
 text \<open>Classical \<open>\<longleftrightarrow>\<close> elimination.\<close>
 lemma iffCE:
diff -r cf96b584724d -r 980cc422526e src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Sep 26 21:55:46 2024 +0200
+++ b/src/HOL/Int.thy	Thu Sep 26 23:04:01 2024 +0200
@@ -1790,11 +1790,11 @@
 lemma power_int_eq_0_iff [simp]: "power_int (x::'a) n = 0 \<longleftrightarrow> x = 0 \<and> n \<noteq> 0"
   by (auto simp: power_int_def)
 
-lemma power_int_0_left_If: "power_int (0 :: 'a) m = (if m = 0 then 1 else 0)"
+lemma power_int_0_left_if: "power_int (0 :: 'a) m = (if m = 0 then 1 else 0)"
   by (auto simp: power_int_def)
 
 lemma power_int_0_left [simp]: "m \<noteq> 0 \<Longrightarrow> power_int (0 :: 'a) m = 0"
-  by (simp add: power_int_0_left_If)
+  by (simp add: power_int_0_left_if)
 
 lemma power_int_1_left [simp]: "power_int 1 n = (1 :: 'a :: division_ring)"
   by (auto simp: power_int_def) 
@@ -1836,7 +1836,7 @@
   shows   "power_int (x::'a) (m + n) = power_int x m * power_int x n"
 proof (cases "x = 0")
   case True
-  thus ?thesis using assms by (auto simp: power_int_0_left_If)
+  thus ?thesis using assms by (auto simp: power_int_0_left_if)
 next
   case [simp]: False
   show ?thesis
@@ -2050,7 +2050,7 @@
   also have "\<dots> \<le> power_int a n * 1"
     using assms * by (intro mult_left_mono) (auto simp: power_int_def)
   finally show ?thesis by simp
-qed (use assms in \<open>auto simp: power_int_0_left_If\<close>)
+qed (use assms in \<open>auto simp: power_int_0_left_if\<close>)
 
 lemma one_less_power_int: "1 < (a :: 'a) \<Longrightarrow> 0 < n \<Longrightarrow> 1 < power_int a n"
   using power_int_strict_increasing[of 0 n a] by simp
diff -r cf96b584724d -r 980cc422526e src/HOL/Power.thy
--- a/src/HOL/Power.thy	Thu Sep 26 21:55:46 2024 +0200
+++ b/src/HOL/Power.thy	Thu Sep 26 23:04:01 2024 +0200
@@ -348,6 +348,10 @@
     by (simp add: power_add)
 qed
 
+lemma power_diff_if:
+  "a ^ (m - n) = (if n \<le> m then (a ^ m) div (a ^ n) else 1)" if "a \<noteq> 0"
+  by (simp add: power_diff that) 
+
 end
 
 context algebraic_semidom
diff -r cf96b584724d -r 980cc422526e src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Thu Sep 26 21:55:46 2024 +0200
+++ b/src/Pure/PIDE/rendering.scala	Thu Sep 26 23:04:01 2024 +0200
@@ -237,6 +237,10 @@
   val warning_elements = Markup.Elements(Markup.WARNING, Markup.LEGACY)
   val error_elements = Markup.Elements(Markup.ERROR)
 
+  val comment_elements =
+    Markup.Elements(Markup.ML_COMMENT, Markup.COMMENT, Markup.COMMENT1, Markup.COMMENT2,
+      Markup.COMMENT3)
+
   val entity_elements = Markup.Elements(Markup.ENTITY)
 
   val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED)
@@ -710,6 +714,12 @@
     snapshot.select(range, Rendering.error_elements, _ => Some(_)).map(_.info)
 
 
+  /* comments */
+
+  def comments(range: Text.Range): List[Text.Markup] =
+    snapshot.select(range, Rendering.comment_elements, _ => Some(_)).map(_.info)
+
+
   /* command status overview */
 
   def overview_color(range: Text.Range): Option[Rendering.Color.Value] = {