changeset 45651 | 172aa230ce69 |
parent 45625 | 750c5a47400b |
child 45909 | 6fe61da4c467 |
--- a/src/HOL/Set.thy Sun Nov 27 21:53:38 2011 +0100 +++ b/src/HOL/Set.thy Sun Nov 27 22:03:22 2011 +0100 @@ -1797,7 +1797,6 @@ val bspec = @{thm bspec} val contra_subsetD = @{thm contra_subsetD} val distinct_lemma = @{thm distinct_lemma} -val eq_to_mono = @{thm eq_to_mono} val equalityCE = @{thm equalityCE} val equalityD1 = @{thm equalityD1} val equalityD2 = @{thm equalityD2}