--- 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
--- a/src/HOL/Sledgehammer.thy Tue Mar 25 09:10:44 2025 +0100
+++ b/src/HOL/Sledgehammer.thy Tue Mar 25 13:42:15 2025 +0100
@@ -7,7 +7,7 @@
section \<open>Sledgehammer: Isabelle--ATP Linkup\<close>
theory Sledgehammer
-imports Presburger SMT
+imports Presburger SMT Try0
keywords
"sledgehammer" :: diag and
"sledgehammer_params" :: thy_decl
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Try0.thy Tue Mar 25 13:42:15 2025 +0100
@@ -0,0 +1,14 @@
+(* Title: HOL/Try0.thy
+ Author: Jasmin Blanchette, LMU Muenchen
+ Author: Martin Desharnais, LMU Muenchen
+ Author: Fabian Huch, TU Muenchen
+*)
+
+theory Try0
+ imports Presburger
+ keywords "try0" :: diag
+begin
+
+ML_file \<open>Tools/try0.ML\<close>
+
+end
\ No newline at end of file