src/HOL/Metis.thy
changeset 39953 aa54f347e5e2
parent 39947 f95834c8bb4d
child 39955 cb9cac7eba29
     1.1 --- a/src/HOL/Metis.thy	Tue Oct 05 11:14:56 2010 +0200
     1.2 +++ b/src/HOL/Metis.thy	Tue Oct 05 11:45:10 2010 +0200
     1.3 @@ -31,4 +31,7 @@
     1.4  use "Tools/Metis/metis_tactics.ML"
     1.5  setup Metis_Tactics.setup
     1.6  
     1.7 +hide_const (open) fequal
     1.8 +hide_fact (open) fequal_imp_equal equal_imp_fequal equal_imp_equal
     1.9 +
    1.10  end