| changeset 1642 | 21db0cf9a1a4 |
| parent 1465 | 5d7a7e439cec |
| child 1844 | 791e79473966 |
--- a/src/HOL/Integ/Equiv.ML Thu Apr 04 11:43:25 1996 +0200 +++ b/src/HOL/Integ/Equiv.ML Thu Apr 04 11:45:01 1996 +0200 @@ -82,7 +82,7 @@ qed "equiv_class_nondisjoint"; val [major] = goalw Equiv.thy [equiv_def,refl_def] - "equiv A r ==> r <= Sigma A (%x.A)"; + "equiv A r ==> r <= A Times A"; by (rtac (major RS conjunct1 RS conjunct1) 1); qed "equiv_type";