src/HOL/Metis.thy
changeset 39955 cb9cac7eba29
parent 39953 aa54f347e5e2
child 39980 f175e482dabe
     1.1 --- a/src/HOL/Metis.thy	Tue Oct 05 12:04:19 2010 +0200
     1.2 +++ b/src/HOL/Metis.thy	Tue Oct 05 12:04:49 2010 +0200
     1.3 @@ -32,6 +32,6 @@
     1.4  setup Metis_Tactics.setup
     1.5  
     1.6  hide_const (open) fequal
     1.7 -hide_fact (open) fequal_imp_equal equal_imp_fequal equal_imp_equal
     1.8 +hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal
     1.9  
    1.10  end