src/HOL/Groebner_Basis.thy
 changeset 30866 dd5117e2d73e parent 30729 461ee3e49ad3 child 30869 71fde5b7b43c
```     1.1 --- a/src/HOL/Groebner_Basis.thy	Fri Apr 03 18:03:29 2009 +0200
1.2 +++ b/src/HOL/Groebner_Basis.thy	Sun Apr 05 05:07:10 2009 +0100
1.3 @@ -191,8 +191,7 @@
1.4
1.5  open Conv;
1.6
1.7 -fun numeral_is_const ct =
1.8 -  can HOLogic.dest_number (Thm.term_of ct);
1.9 +fun numeral_is_const ct = can HOLogic.dest_number (Thm.term_of ct);
1.10
1.11  fun int_of_rat x =
1.12    (case Rat.quotient_of_rat x of (i, 1) => i
1.13 @@ -260,16 +259,22 @@
1.14  locale gb_field = gb_ring +
1.15    fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.16      and inverse:: "'a \<Rightarrow> 'a"
1.17 -  assumes divide: "divide x y = mul x (inverse y)"
1.18 -     and inverse: "inverse x = divide r1 x"
1.19 +  assumes divide_inverse: "divide x y = mul x (inverse y)"
1.20 +     and inverse_divide: "inverse x = divide r1 x"
1.21  begin
1.22
1.23 +lemma field_ops: shows "TERM (divide x y)" and "TERM (inverse x)" .
1.24 +
1.25 +lemmas field_rules = divide_inverse inverse_divide
1.26 +
1.27  lemmas gb_field_axioms' =
1.28    gb_field_axioms [normalizer
1.29      semiring ops: semiring_ops
1.30      semiring rules: semiring_rules
1.31      ring ops: ring_ops
1.32 -    ring rules: ring_rules]
1.33 +    ring rules: ring_rules
1.34 +    field ops: field_ops
1.35 +    field rules: field_rules]
1.36
1.37  end
1.38
1.39 @@ -393,6 +398,8 @@
1.40    semiring rules: semiring_rules
1.41    ring ops: ring_ops
1.42    ring rules: ring_rules
1.43 +  field ops: field_ops
1.44 +  field rules: field_rules