src/HOL/Metis.thy
changeset 39980 f175e482dabe
parent 39955 cb9cac7eba29
child 41042 8275f52ac991
     1.1 --- a/src/HOL/Metis.thy	Mon Oct 11 18:03:18 2010 +0700
     1.2 +++ b/src/HOL/Metis.thy	Mon Oct 11 18:03:47 2010 +0700
     1.3 @@ -29,7 +29,11 @@
     1.4  use "Tools/Metis/metis_translate.ML"
     1.5  use "Tools/Metis/metis_reconstruct.ML"
     1.6  use "Tools/Metis/metis_tactics.ML"
     1.7 -setup Metis_Tactics.setup
     1.8 +
     1.9 +setup {*
    1.10 +  Metis_Reconstruct.setup
    1.11 +  #> Metis_Tactics.setup
    1.12 +*}
    1.13  
    1.14  hide_const (open) fequal
    1.15  hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal