changeset 803 | 4c8333ab3eae |
parent 782 | 200a16083201 |
child 858 | b87867b3fd91 |
--- a/src/ZF/Sum.ML Fri Dec 16 17:46:02 1994 +0100 +++ b/src/ZF/Sum.ML Fri Dec 16 18:07:12 1994 +0100 @@ -165,8 +165,7 @@ by (fast_tac (sum_cs addSIs [equalityI]) 1); qed "Part_Collect"; -val Part_CollectE = - Part_Collect RS equalityD1 RS subsetD RS CollectE |> standard; +bind_thm ("Part_CollectE", Part_Collect RS equalityD1 RS subsetD RS CollectE); goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}"; by (fast_tac (sum_cs addIs [equalityI]) 1);