--- a/src/HOL/Groebner_Basis.thy Mon Oct 27 18:14:34 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy Tue Oct 28 11:03:07 2008 +0100
@@ -64,7 +64,7 @@
subsubsection {* Declaring the abstract theory *}
lemma semiring_ops:
- includes meta_term_syntax
+ fixes meta_term :: "'a => prop" ("TERM _")
shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)"
and "TERM r0" and "TERM r1"
by rule+
@@ -227,7 +227,7 @@
begin
lemma ring_ops:
- includes meta_term_syntax
+ fixes meta_term :: "'a => prop" ("TERM _")
shows "TERM (sub x y)" and "TERM (neg x)" .
lemmas ring_rules = neg_mul sub_add