src/HOL/Presburger.thy

--- a/src/HOL/Presburger.thy	Sun May 04 18:50:42 2014 +0200
+++ b/src/HOL/Presburger.thy	Sun May 04 18:53:58 2014 +0200
@@ -434,5 +434,9 @@
 lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
 lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
 
+
+subsection {* Try0 *}
+
+ML_file "Tools/try0.ML"
+
 end
-