src/HOL/Metis.thy
changeset 41042 8275f52ac991
parent 39980 f175e482dabe
child 41140 9c68004b8c9d
     1.1 --- a/src/HOL/Metis.thy	Tue Dec 07 09:58:52 2010 +0100
     1.2 +++ b/src/HOL/Metis.thy	Tue Dec 07 09:58:56 2010 +0100
     1.3 @@ -12,6 +12,7 @@
     1.4       ("Tools/Metis/metis_translate.ML")
     1.5       ("Tools/Metis/metis_reconstruct.ML")
     1.6       ("Tools/Metis/metis_tactics.ML")
     1.7 +     ("Tools/try.ML")
     1.8  begin
     1.9  
    1.10  definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    1.11 @@ -38,4 +39,10 @@
    1.12  hide_const (open) fequal
    1.13  hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal
    1.14  
    1.15 +subsection {* Try *}
    1.16 +
    1.17 +use "Tools/try.ML"
    1.18 +
    1.19 +setup {* Try.setup *}
    1.20 +
    1.21  end