1.1 --- a/src/HOL/Integ/cooper_proof.ML	Tue Apr 08 09:40:30 2003 +0200
     1.2 +++ b/src/HOL/Integ/cooper_proof.ML	Tue Apr 08 09:44:21 2003 +0200
     1.3 @@ -274,7 +274,7 @@
     1.4         val m = l div (dest_numeral c) 
     1.5         val n = abs (m)
     1.6         val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x)) 
     1.7 -       val rs = (HOLogic.mk_binrel "op <" (zero,linear_sub [] one (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
     1.8 +       val rs = (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
     1.9         in (ACPI(n,fm),rs)
    1.10         end
    1.11    else  let val rs = (HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt )) 
    1.12 @@ -765,21 +765,21 @@
    1.13       val cx = cterm_of sg x
    1.14       val ca = cterm_of sg a
    1.15     in case p of
    1.16 -     "op <" => let val pre = prove_elementar sg "ss" 
    1.17 +     "op <" => let val pre = prove_elementar sg "lf" 
    1.18  	                  (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
    1.19  	           val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_lt_eq)))
    1.20 -		      in [th1,(prove_elementar sg "ss" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
    1.21 +		      in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
    1.22                     end
    1.23 -    |"op =" =>let val pre = prove_elementar sg "ss" 
    1.24 +    |"op =" =>let val pre = prove_elementar sg "lf" 
    1.25  	    (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
    1.26  	          in let val th1 = (pre RS(instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_eq_eq)))
    1.27 -	             in [th1,(prove_elementar sg "ss" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
    1.28 +	             in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
    1.29                        end
    1.30                    end
    1.31 -    |"Divides.op dvd" =>let val pre = prove_elementar sg "ss" 
    1.32 +    |"Divides.op dvd" =>let val pre = prove_elementar sg "lf" 
    1.33  	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
    1.34  	                 val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct]) (ac_dvd_eq))
    1.35 -                         in [th1,(prove_elementar sg "ss" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
    1.36 +                         in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
    1.37                          
    1.38                            end
    1.39    end
    1.40 @@ -789,7 +789,7 @@
    1.41       val cc = cterm_of sg c
    1.42       val ct = cterm_of sg t
    1.43       val cx = cterm_of sg x
    1.44 -     val pre = prove_elementar sg "ss" 
    1.45 +     val pre = prove_elementar sg "lf" 
    1.46         (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
    1.47         val th1 = (pre RS (instantiate' [] [Some ck,Some cc, Some cx, Some ct] (ac_pi_eq)))
    1.48