--- 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