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