# HG changeset patch # User blanchet # Date 1286795027 -25200 # Node ID f175e482dabebdc3d7a606d56c9d35afbf29e087 # Parent b13515940b53616b7b1645d2efb58a7edbd0d97a "setup" in theory diff -r b13515940b53 -r f175e482dabe src/HOL/Metis.thy --- a/src/HOL/Metis.thy Mon Oct 11 18:03:18 2010 +0700 +++ b/src/HOL/Metis.thy Mon Oct 11 18:03:47 2010 +0700 @@ -29,7 +29,11 @@ use "Tools/Metis/metis_translate.ML" use "Tools/Metis/metis_reconstruct.ML" use "Tools/Metis/metis_tactics.ML" -setup Metis_Tactics.setup + +setup {* + Metis_Reconstruct.setup + #> Metis_Tactics.setup +*} hide_const (open) fequal hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal