added Clarify_tac to speed up proofs

--- 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";
 

--- 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";
 

--- 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();