# HG changeset patch
# User Andreas Lochbihler
# Date 1447243021 -3600
# Node ID c657ee4f59b7edd84c34b8e06d81bb718ce49c17
# Parent  48e2de1b1df52b1a905a1a7db9fad628d2fa0a4e
adapt to 90f54d9e63f2

diff -r 48e2de1b1df5 -r c657ee4f59b7 src/HOL/UNITY/Detects.thy
--- a/src/HOL/UNITY/Detects.thy	Wed Nov 11 10:28:22 2015 +0100
+++ b/src/HOL/UNITY/Detects.thy	Wed Nov 11 12:57:01 2015 +0100
@@ -20,6 +20,7 @@
 
 lemma Always_at_FP:
      "[|F \<in> A LeadsTo B; all_total F|] ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
+supply [[simproc del: boolean_algebra_cancel_inf]] inf_compl_bot_right[simp del] 
 apply (rule LeadsTo_empty)
 apply (subgoal_tac "F \<in> (FP F \<inter> A \<inter> - B) LeadsTo (B \<inter> (FP F \<inter> -B))")
 apply (subgoal_tac [2] " (FP F \<inter> A \<inter> - B) = (A \<inter> (FP F \<inter> -B))")