src/HOL/UNITY/WFair.ML
changeset 5669 f5d9caafc3bd
parent 5648 fe887910e32e
child 5971 c5a7a7685826
     1.1 --- a/src/HOL/UNITY/WFair.ML	Mon Oct 19 11:25:37 1998 +0200
     1.2 +++ b/src/HOL/UNITY/WFair.ML	Mon Oct 19 11:26:46 1998 +0200
     1.3 @@ -421,6 +421,7 @@
     1.4  \      F : constrains (A1 - B) (A1 Un B); \
     1.5  \      F : constrains (A2 - C) (A2 Un C) |] \
     1.6  \   ==> F : constrains (A1 Un A2 - C) (A1 Un A2 Un C)";
     1.7 +by (Clarify_tac 1);
     1.8  by (Blast_tac 1);
     1.9  val lemma1 = result();
    1.10