src/HOL/Groebner_Basis.thy
changeset 28699 32b6a8f12c1c
parent 28402 09e4aa3ddc25
child 28823 dcbef866c9e2
     1.1 --- a/src/HOL/Groebner_Basis.thy	Mon Oct 27 18:14:34 2008 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Oct 28 11:03:07 2008 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4  subsubsection {* Declaring the abstract theory *}
     1.5  
     1.6  lemma semiring_ops:
     1.7 -  includes meta_term_syntax
     1.8 +  fixes meta_term :: "'a => prop"  ("TERM _")
     1.9    shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)"
    1.10      and "TERM r0" and "TERM r1"
    1.11    by rule+
    1.12 @@ -227,7 +227,7 @@
    1.13  begin
    1.14  
    1.15  lemma ring_ops:
    1.16 -  includes meta_term_syntax
    1.17 +  fixes meta_term :: "'a => prop"  ("TERM _")
    1.18    shows "TERM (sub x y)" and "TERM (neg x)" .
    1.19  
    1.20  lemmas ring_rules = neg_mul sub_add