author | blanchet |
Tue, 05 Oct 2010 12:04:49 +0200 | |
changeset 39955 | cb9cac7eba29 |
parent 39954 | 1a908a35920b |
child 39956 | 132b79985660 |
src/HOL/Metis.thy | file | annotate | diff | comparison | revisions |
--- 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