author | blanchet |
Mon, 11 Oct 2010 18:03:47 +0700 | |
changeset 39980 | f175e482dabe |
parent 39979 | b13515940b53 |
child 39988 | a4b2971952f4 |
src/HOL/Metis.thy | file | annotate | diff | comparison | revisions |
--- 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