--- a/Set.ML Fri Jun 24 15:11:39 1994 +0200
+++ b/Set.ML Wed Jun 29 12:04:04 1994 +0200
@@ -117,10 +117,10 @@
(*Takes assumptions A<=B; c:A and creates the assumption c:B *)
fun set_mp_tac i = etac subsetCE i THEN mp_tac i;
-val subset_refl = prove_goal Set.thy "A <= A::'a set"
+val subset_refl = prove_goal Set.thy "A <= (A::'a set)"
(fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]);
-val prems = goal Set.thy "[| A<=B; B<=C |] ==> A<=C::'a set";
+val prems = goal Set.thy "[| A<=B; B<=C |] ==> A<=(C::'a set)";
by (cut_facts_tac prems 1);
by (REPEAT (ares_tac [subsetI] 1 ORELSE set_mp_tac 1));
val subset_trans = result();
@@ -129,25 +129,25 @@
(*** Equality ***)
(*Anti-symmetry of the subset relation*)
-val prems = goal Set.thy "[| A <= B; B <= A |] ==> A = B::'a set";
+val prems = goal Set.thy "[| A <= B; B <= A |] ==> A = (B::'a set)";
by (rtac (iffI RS set_ext) 1);
by (REPEAT (ares_tac (prems RL [subsetD]) 1));
val subset_antisym = result();
val equalityI = subset_antisym;
(* Equality rules from ZF set theory -- are they appropriate here? *)
-val prems = goal Set.thy "A = B ==> A<=B::'a set";
+val prems = goal Set.thy "A = B ==> A<=(B::'a set)";
by (resolve_tac (prems RL [subst]) 1);
by (rtac subset_refl 1);
val equalityD1 = result();
-val prems = goal Set.thy "A = B ==> B<=A::'a set";
+val prems = goal Set.thy "A = B ==> B<=(A::'a set)";
by (resolve_tac (prems RL [subst]) 1);
by (rtac subset_refl 1);
val equalityD2 = result();
val prems = goal Set.thy
- "[| A = B; [| A<=B; B<=A::'a set |] ==> P |] ==> P";
+ "[| A = B; [| A<=B; B<=(A::'a set) |] ==> P |] ==> P";
by (resolve_tac prems 1);
by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
val equalityE = result();