src/HOL/arith_data.ML
changeset 11464 ddea204de5bc
parent 11334 a16eaf2a1edd
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/arith_data.ML	Mon Aug 06 13:12:06 2001 +0200
     1.2 +++ b/src/HOL/arith_data.ML	Mon Aug 06 13:43:24 2001 +0200
     1.3 @@ -299,6 +299,7 @@
     1.4        else poly(s,m,poly(t,ratneg m,pi))
     1.5    | poly(Const("uminus",_) $ t, m, pi) = poly(t,ratneg m,pi)
     1.6    | poly(Const("0",_), _, pi) = pi
     1.7 +  | poly(Const("1",_), m, (p,i)) = (p,ratadd(i,m))
     1.8    | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,ratadd(i,m)))
     1.9    | poly(t as Const("op *",_) $ _ $ _, m, pi as (p,i)) =
    1.10        (case demult(t,m) of
    1.11 @@ -363,7 +364,7 @@
    1.12  (* reduce contradictory <= to False.
    1.13     Most of the work is done by the cancel tactics.
    1.14  *)
    1.15 -val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq];
    1.16 +val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,One_def];
    1.17  
    1.18  val add_mono_thms_nat = map (fn s => prove_goal (the_context ()) s
    1.19   (fn prems => [cut_facts_tac prems 1,