equal
deleted
inserted
replaced
134 *) |
134 *) |
135 |
135 |
136 end; |
136 end; |
137 |
137 |
138 |
138 |
139 (* Some test data [omitting examples that assume the ordering to be discrete!] |
139 (* SOME test data [omitting examples that assume the ordering to be discrete!] |
140 Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"; |
140 Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"; |
141 by (fast_arith_tac 1); |
141 by (fast_arith_tac 1); |
142 qed ""; |
142 qed ""; |
143 |
143 |
144 Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c"; |
144 Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c"; |