--- a/src/HOL/Metis.thy Tue Dec 07 09:58:52 2010 +0100
+++ b/src/HOL/Metis.thy Tue Dec 07 09:58:56 2010 +0100
@@ -12,6 +12,7 @@
("Tools/Metis/metis_translate.ML")
("Tools/Metis/metis_reconstruct.ML")
("Tools/Metis/metis_tactics.ML")
+ ("Tools/try.ML")
begin
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
@@ -38,4 +39,10 @@
hide_const (open) fequal
hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal
+subsection {* Try *}
+
+use "Tools/try.ML"
+
+setup {* Try.setup *}
+
end