# HG changeset patch
# User wenzelm
# Date 1315684075 -7200
# Node ID 0d23a8ae14df28e92b768fb73058486e489fe5cf
# Parent  328825888426fcd787ead32d56cf33d40f0a711d
speed up slow proof;

diff -r 328825888426 -r 0d23a8ae14df src/HOL/UNITY/Constrains.thy
--- a/src/HOL/UNITY/Constrains.thy	Sat Sep 10 20:41:27 2011 +0200
+++ b/src/HOL/UNITY/Constrains.thy	Sat Sep 10 21:47:55 2011 +0200
@@ -181,7 +181,9 @@
 
 lemma Constrains_cancel:
      "[| F \<in> A Co (A' \<union> B); F \<in> B Co B' |] ==> F \<in> A Co (A' \<union> B')"
-by (simp add: Constrains_eq_constrains constrains_def, blast)
+apply (simp add: Constrains_eq_constrains constrains_def)
+apply best
+done
 
 
 subsection{*Stable*}