--- a/src/HOL/Presburger.thy	Tue Mar 25 09:10:44 2025 +0100
+++ b/src/HOL/Presburger.thy	Tue Mar 25 13:42:15 2025 +0100
@@ -6,7 +6,6 @@
 
 theory Presburger
 imports Groebner_Basis Set_Interval
-keywords "try0" :: diag
 begin
 
 ML_file \<open>Tools/Qelim/qelim.ML\<close>
@@ -558,9 +557,4 @@
   "n mod 4 = Suc 0 \<Longrightarrow> even ((n - Suc 0) div 2)"
   by presburger
 
-
-subsection \<open>Try0\<close>
-
-ML_file \<open>Tools/try0.ML\<close>
-
 end