| changeset 5189 | 362e4d6213c5 |
| parent 5148 | 74919e8f221c |
| child 5233 | 3571ff68ceda |
--- a/src/HOL/equalities.ML Fri Jul 24 13:34:59 1998 +0200 +++ b/src/HOL/equalities.ML Fri Jul 24 13:35:47 1998 +0200 @@ -727,6 +727,11 @@ by (ALLGOALS Blast_tac); qed "Pow_insert"; +(** for datatypes **) +Goal "f x ~= f y ==> x ~= y"; +by (Fast_tac 1); +qed "distinct_lemma"; + (** Miniscoping: pushing in big Unions and Intersections **) local