--- a/src/HOL/Groebner_Basis.thy Wed Nov 19 18:15:31 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy Thu Nov 20 00:03:47 2008 +0100
@@ -64,10 +64,8 @@
subsubsection {* Declaring the abstract theory *}
lemma semiring_ops:
- 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+
+ and "TERM r0" and "TERM r1" .
lemma semiring_rules:
"add (mul a m) (mul b m) = mul (add a b) m"
@@ -226,9 +224,7 @@
and sub_add: "sub x y = add x (neg y)"
begin
-lemma ring_ops:
- fixes meta_term :: "'a => prop" ("TERM _")
- shows "TERM (sub x y)" and "TERM (neg x)" .
+lemma ring_ops: shows "TERM (sub x y)" and "TERM (neg x)" .
lemmas ring_rules = neg_mul sub_add