--- a/src/HOL/Bali/Eval.thy Sat Jun 17 17:01:51 2017 +0200
+++ b/src/HOL/Bali/Eval.thy Sat Jun 17 20:24:22 2017 +0200
@@ -191,7 +191,6 @@
defer
apply (case_tac "a' = Null")
apply simp_all
-apply iprover
done
definition
--- a/src/HOL/HOL.thy Sat Jun 17 17:01:51 2017 +0200
+++ b/src/HOL/HOL.thy Sat Jun 17 20:24:22 2017 +0200
@@ -927,6 +927,7 @@
"\<And>P. (\<exists>x. t = x \<and> P x) = P t"
"\<And>P. (\<forall>x. x = t \<longrightarrow> P x) = P t"
"\<And>P. (\<forall>x. t = x \<longrightarrow> P x) = P t"
+ "(\<forall>x. x \<noteq> t) = False" "(\<forall>x. t \<noteq> x) = False"
by (blast, blast, blast, blast, blast, iprover+)
lemma disj_absorb: "A \<or> A \<longleftrightarrow> A"
--- a/src/HOL/ex/Bubblesort.thy Sat Jun 17 17:01:51 2017 +0200
+++ b/src/HOL/ex/Bubblesort.thy Sat Jun 17 20:24:22 2017 +0200
@@ -45,7 +45,7 @@
apply(induction xs rule: bubble_min.induct)
apply simp
apply simp
-apply (auto simp: add_eq_conv_ex split: list.split)
+apply (auto split: list.split)
done
lemma bubble_minD_mset: