src/HOL/Integ/int_arith1.ML
changeset 15661 9ef583b08647
parent 15531 08c8dad8e399
child 15921 b6e345548913
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Thu Apr 07 09:24:35 2005 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Thu Apr 07 09:25:33 2005 +0200
     1.3 @@ -538,7 +538,7 @@
     1.4  Addsimprocs [fast_int_arith_simproc]
     1.5  
     1.6  
     1.7 -(* SOME test data
     1.8 +(* Some test data
     1.9  Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
    1.10  by (fast_arith_tac 1);
    1.11  Goal "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)";