# HG changeset patch
# User berghofe
# Date 901280147 -7200
# Node ID 362e4d6213c57f8d455a2ccd1b6db53a082c3aec
# Parent  633ec5f6c1554dd6110d962135a54e0b2f255c50
Added theorem distinct_lemma (needed for datatypes).

diff -r 633ec5f6c155 -r 362e4d6213c5 src/HOL/equalities.ML
--- 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