# HG changeset patch
# User paulson
# Date 908789206 -7200
# Node ID f5d9caafc3bd8488ad556c648761f782655cf53e
# Parent  9ddc4e836d3e1b5c21091e2c58eafd6ace5c1cfa
added Clarify_tac to speed up proofs

diff -r 9ddc4e836d3e -r f5d9caafc3bd src/HOL/UNITY/Constrains.ML
--- a/src/HOL/UNITY/Constrains.ML	Mon Oct 19 11:25:37 1998 +0200
+++ b/src/HOL/UNITY/Constrains.ML	Mon Oct 19 11:26:46 1998 +0200
@@ -170,6 +170,7 @@
 Goalw [Constrains_def, constrains_def]
    "[| F : Constrains A (A' Un B); F : Constrains B B' |] \
 \   ==> F : Constrains A (A' Un B')";
+by (Clarify_tac 1);
 by (Blast_tac 1);
 qed "Constrains_cancel";
 
diff -r 9ddc4e836d3e -r f5d9caafc3bd src/HOL/UNITY/UNITY.ML
--- a/src/HOL/UNITY/UNITY.ML	Mon Oct 19 11:25:37 1998 +0200
+++ b/src/HOL/UNITY/UNITY.ML	Mon Oct 19 11:26:46 1998 +0200
@@ -224,6 +224,7 @@
 Goalw [constrains_def]
    "[| F : constrains A (A' Un B); F : constrains B B' |] \
 \   ==> F : constrains A (A' Un B')";
+by (Clarify_tac 1);
 by (Blast_tac 1);
 qed "constrains_cancel";
 
diff -r 9ddc4e836d3e -r f5d9caafc3bd src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Mon Oct 19 11:25:37 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML	Mon Oct 19 11:26:46 1998 +0200
@@ -421,6 +421,7 @@
 \      F : constrains (A1 - B) (A1 Un B); \
 \      F : constrains (A2 - C) (A2 Un C) |] \
 \   ==> F : constrains (A1 Un A2 - C) (A1 Un A2 Un C)";
+by (Clarify_tac 1);
 by (Blast_tac 1);
 val lemma1 = result();