merged
authorwenzelm
Fri, 08 Jan 2021 20:40:56 +0100
changeset 73107 f062d19c4b44
parent 73104 6520d59fbdd7 (diff)
parent 73106 3df45de0c079 (current diff)
child 73108 981a383610df
merged
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Fri Jan 08 16:59:27 2021 +0100
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Fri Jan 08 20:40:56 2021 +0100
@@ -1606,6 +1606,9 @@
   thus ?thesis by simp
 qed
 
+lemma multiplicity_zero_1 [simp]: "multiplicity 0 x = 0"
+  by (metis (mono_tags) local.dvd_0_left multiplicity_zero not_dvd_imp_multiplicity_0)
+
 lemma inj_on_Prod_primes:
   assumes "\<And>P p. P \<in> A \<Longrightarrow> p \<in> P \<Longrightarrow> prime p"
   assumes "\<And>P. P \<in> A \<Longrightarrow> finite P"
--- a/src/HOL/Tools/SMT/smt_systems.ML	Fri Jan 08 16:59:27 2021 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Fri Jan 08 20:40:56 2021 +0100
@@ -35,8 +35,15 @@
     " failed -- enable tracing using the " ^ quote (Config.name_of SMT_Config.trace) ^
     " option for details"))
 
+(* When used with bitvectors, CVC4 can produce error messages like:
+
+$ISABELLE_TMP_PREFIX/... No set-logic command was given before this point.
+
+These message should be ignored.
+*)
 fun is_blank_or_error_line "" = true
-  | is_blank_or_error_line s = String.isPrefix "(error " s
+  | is_blank_or_error_line s =
+  String.isPrefix "(error " s orelse String.isPrefix (getenv "ISABELLE_TMP_PREFIX") s
 
 fun on_first_line test_outcome solver_name lines =
   let