"setup" in theory
authorblanchet
Mon, 11 Oct 2010 18:03:47 +0700
changeset 39980 f175e482dabe
parent 39979 b13515940b53
child 39988 a4b2971952f4
"setup" in theory
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