--- a/src/HOL/Groebner_Basis.thy Thu Jan 30 13:38:28 2014 +0100
+++ b/src/HOL/Groebner_Basis.thy Thu Jan 30 13:38:28 2014 +0100
@@ -85,4 +85,9 @@
declare zmod_eq_dvd_iff[algebra]
declare nat_mod_eq_iff[algebra]
+
+subsection {* Try0 *}
+
+ML_file "Tools/try0.ML"
+
end