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