src/HOL/UNITY/Constrains.ML
changeset 5669 f5d9caafc3bd
parent 5648 fe887910e32e
child 5784 54276fba8420
     1.1 --- a/src/HOL/UNITY/Constrains.ML	Mon Oct 19 11:25:37 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Constrains.ML	Mon Oct 19 11:26:46 1998 +0200
     1.3 @@ -170,6 +170,7 @@
     1.4  Goalw [Constrains_def, constrains_def]
     1.5     "[| F : Constrains A (A' Un B); F : Constrains B B' |] \
     1.6  \   ==> F : Constrains A (A' Un B')";
     1.7 +by (Clarify_tac 1);
     1.8  by (Blast_tac 1);
     1.9  qed "Constrains_cancel";
    1.10