# HG changeset patch
# User nipkow
# Date 1497723862 -7200
# Node ID 20304512a33b8b298ae1129c410d834456e652e4
# Parent  8b433b6f302f727b9991930fa8af05f1b8b2fa59# Parent  d59f9f6961105d455bd5f7005e18f69d8ce4db78
merged

diff -r 8b433b6f302f -r 20304512a33b src/HOL/Bali/Eval.thy
--- 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
diff -r 8b433b6f302f -r 20304512a33b src/HOL/HOL.thy
--- 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"
diff -r 8b433b6f302f -r 20304512a33b src/HOL/ex/Bubblesort.thy
--- 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: