--- 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:
--- 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:
--- 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
--- 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
--- 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] = {