tuned;
authorwenzelm
Thu Jul 05 00:06:19 2007 +0200 (2007-07-05)
changeset 23581297c6d706322
parent 23580 998a6fda9bb6
child 23582 94d0dd87cc24
tuned;
src/HOL/Tools/Groebner_Basis/normalizer_data.ML
src/HOL/ex/Groebner_Examples.thy
     1.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Thu Jul 05 00:06:18 2007 +0200
     1.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Thu Jul 05 00:06:19 2007 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  signature NORMALIZER_DATA =
     1.5  sig
     1.6    type entry
     1.7 -  val get: Proof.context -> simpset * ((thm * entry) list)
     1.8 +  val get: Proof.context -> simpset * (thm * entry) list
     1.9    val match: Proof.context -> cterm -> entry option
    1.10    val del: attribute
    1.11    val add: {semiring: cterm list * thm list, ring: cterm list * thm list, idom: thm list}
    1.12 @@ -41,11 +41,11 @@
    1.13  
    1.14  structure Data = GenericDataFun
    1.15  (
    1.16 -  type T = simpset * ((thm * entry) list);
    1.17 +  type T = simpset * (thm * entry) list;
    1.18    val empty = (HOL_basic_ss, []);
    1.19    val extend = I;
    1.20 -  fun merge _ ((ss, e), (ss', e')) = (merge_ss (ss, ss'), 
    1.21 -                                      AList.merge eq_key (K true) (e,e'));
    1.22 +  fun merge _ ((ss, e), (ss', e')) =
    1.23 +    (merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e'));
    1.24  );
    1.25  
    1.26  val get = Data.get o Context.Proof;
    1.27 @@ -134,7 +134,6 @@
    1.28        val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
    1.29  
    1.30        val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
    1.31 -      val _ = map print_thm sr_rules';
    1.32        val semiring = (sr_ops, sr_rules');
    1.33        val ring = (r_ops, r_rules');
    1.34      in
     2.1 --- a/src/HOL/ex/Groebner_Examples.thy	Thu Jul 05 00:06:18 2007 +0200
     2.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Thu Jul 05 00:06:19 2007 +0200
     2.3 @@ -46,9 +46,10 @@
     2.4  theorem "x* (x\<twosuperior> - x  - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)"
     2.5    by algebra
     2.6  
     2.7 -lemma fixes x::"'a::{idom,recpower,number_ring}"
     2.8 -shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow>  x=1 & y=1 | x=0 & y=0"
     2.9 -by algebra
    2.10 +lemma
    2.11 +  fixes x::"'a::{idom,recpower,number_ring}"
    2.12 +  shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow>  x=1 & y=1 | x=0 & y=0"
    2.13 +  by algebra
    2.14  
    2.15  subsection {* Lemmas for Lagrange's theorem *}
    2.16