| changeset 90 | 5c7a69cef18b |
| parent 57 | 194d088c1511 |
| child 171 | 16c4ea954511 |
--- a/subset.ML Fri Jun 24 15:11:39 1994 +0200 +++ b/subset.ML Wed Jun 29 12:04:04 1994 +0200 @@ -117,7 +117,7 @@ (*** Set difference ***) -val Diff_subset = prove_goal Set.thy "A-B <= A::'a set" +val Diff_subset = prove_goal Set.thy "A-B <= (A::'a set)" (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac DiffE 1)) ]); (*** Monotonicity ***)