# HG changeset patch
# User desharna
# Date 1742906535 -3600
# Node ID 56098b36c49f7a7305963b5901537b83dfe0393c
# Parent  4238ebc9918d94c9500acb9504969a0c7afb8e11
moved command try0 into its own new theory

diff -r 4238ebc9918d -r 56098b36c49f src/HOL/Presburger.thy
--- 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
diff -r 4238ebc9918d -r 56098b36c49f src/HOL/Sledgehammer.thy
--- 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
diff -r 4238ebc9918d -r 56098b36c49f src/HOL/Try0.thy
--- /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