--- a/src/HOL/Groebner_Basis.thy Thu Nov 06 16:10:33 2014 +0100
+++ b/src/HOL/Groebner_Basis.thy Fri Nov 07 15:19:30 2014 +0100
@@ -6,7 +6,6 @@
theory Groebner_Basis
imports Semiring_Normalization Parity
-keywords "try0" :: diag
begin
subsection {* Groebner Bases *}
--- a/src/HOL/Presburger.thy Thu Nov 06 16:10:33 2014 +0100
+++ b/src/HOL/Presburger.thy Fri Nov 07 15:19:30 2014 +0100
@@ -6,6 +6,7 @@
theory Presburger
imports Groebner_Basis Set_Interval
+keywords "try0" :: diag
begin
ML_file "Tools/Qelim/qelim.ML"