src/HOL/Set.thy
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}