# HG changeset patch
# User wenzelm
# Date 1392569413 -3600
# Node ID a3870c12f254172d1daee474247d1be0e8afc85d
# Parent  bd67ebe275e0bdfb4ff26606b6e1a8b166a67439# Parent  d0157612ebe588bbeab8c94d817c45b3e5b6f673
merged

diff -r d0157612ebe5 -r a3870c12f254 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Sun Feb 16 17:25:03 2014 +0100
+++ b/src/HOL/Groebner_Basis.thy	Sun Feb 16 17:50:13 2014 +0100
@@ -6,6 +6,7 @@
 
 theory Groebner_Basis
 imports Semiring_Normalization
+keywords "try0" :: diag
 begin
 
 subsection {* Groebner Bases *}
diff -r d0157612ebe5 -r a3870c12f254 src/HOL/Metis.thy
--- a/src/HOL/Metis.thy	Sun Feb 16 17:25:03 2014 +0100
+++ b/src/HOL/Metis.thy	Sun Feb 16 17:50:13 2014 +0100
@@ -8,7 +8,6 @@
 
 theory Metis
 imports ATP
-keywords "try0" :: diag
 begin
 
 ML_file "~~/src/Tools/Metis/metis.ML"