--- a/src/HOL/Fields.thy Mon Mar 23 10:16:20 2015 +0100
+++ b/src/HOL/Fields.thy Mon Mar 23 15:08:02 2015 +0100
@@ -30,8 +30,8 @@
begin
lemma [field_simps]:
- shows distrib_left_NO_MATCH: "NO_MATCH a (x / y) \<Longrightarrow> a * (b + c) = a * b + a * c"
- and distrib_right_NO_MATCH: "NO_MATCH c (x / y) \<Longrightarrow> (a + b) * c = a * c + b * c"
+ shows distrib_left_NO_MATCH: "NO_MATCH (x / y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
+ and distrib_right_NO_MATCH: "NO_MATCH (x / y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
by (rule distrib_left distrib_right)+
end
@@ -40,8 +40,8 @@
begin
lemma [field_simps]:
- shows left_diff_distrib_NO_MATCH: "NO_MATCH c (x / y) \<Longrightarrow> (a - b) * c = a * c - b * c"
- and right_diff_distrib_NO_MATCH: "NO_MATCH a (x / y) \<Longrightarrow> a * (b - c) = a * b - a * c"
+ shows left_diff_distrib_NO_MATCH: "NO_MATCH (x / y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
+ and right_diff_distrib_NO_MATCH: "NO_MATCH (x / y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
by (rule left_diff_distrib right_diff_distrib)+
end
--- a/src/HOL/HOL.thy Mon Mar 23 10:16:20 2015 +0100
+++ b/src/HOL/HOL.thy Mon Mar 23 15:08:02 2015 +0100
@@ -1671,13 +1671,13 @@
The simplification procedure can be used to avoid simplification of terms of a certain form
*}
-definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH val pat \<equiv> True"
+definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH pat val \<equiv> True"
-lemma NO_MATCH_cong[cong]: "NO_MATCH val pat = NO_MATCH val pat" by (rule refl)
+lemma NO_MATCH_cong[cong]: "NO_MATCH pat val = NO_MATCH pat val" by (rule refl)
declare [[coercion_args NO_MATCH - -]]
-simproc_setup NO_MATCH ("NO_MATCH val pat") = {* fn _ => fn ctxt => fn ct =>
+simproc_setup NO_MATCH ("NO_MATCH pat val") = {* fn _ => fn ctxt => fn ct =>
let
val thy = Proof_Context.theory_of ctxt
val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)
@@ -1686,7 +1686,7 @@
*}
text {*
- This setup ensures that a rewrite rule of the form @{term "NO_MATCH val pat \<Longrightarrow> t"}
+ This setup ensures that a rewrite rule of the form @{term "NO_MATCH pat val \<Longrightarrow> t"}
is only applied, if the pattern @{term pat} does not match the value @{term val}.
*}
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Mon Mar 23 10:16:20 2015 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Mon Mar 23 15:08:02 2015 +0100
@@ -1955,7 +1955,7 @@
qed
lemma nn_integral_count_space_indicator:
- assumes "NO_MATCH (X::'a set) (UNIV::'a set)"
+ assumes "NO_MATCH (UNIV::'a set) (X::'a set)"
shows "(\<integral>\<^sup>+x. f x \<partial>count_space X) = (\<integral>\<^sup>+x. f x * indicator X x \<partial>count_space UNIV)"
by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space)