hide all-too-popular constant name eq
authorhaftmann
Mon Aug 30 09:37:43 2010 +0200 (2010-08-30)
changeset 388668ffb9f541285
parent 38865 43c934dd4bc3
child 38867 23af89f419bb
hide all-too-popular constant name eq
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Mon Aug 30 09:35:30 2010 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Aug 30 09:37:43 2010 +0200
     1.3 @@ -1875,8 +1875,6 @@
     1.4    Nbe.add_const_alias @{thm equal_alias_cert}
     1.5  *}
     1.6  
     1.7 -hide_const (open) equal
     1.8 -
     1.9  text {* Cases *}
    1.10  
    1.11  lemma Let_case_cert:
    1.12 @@ -2127,4 +2125,6 @@
    1.13  
    1.14  *}
    1.15  
    1.16 +hide_const (open) eq equal
    1.17 +
    1.18  end