author | wenzelm |
Tue, 27 Jul 1999 22:04:30 +0200 | |
changeset 7108 | 0229ce6735f6 |
parent 7107 | ce69de572bca |
child 7109 | b02c6bdda05b |
src/HOL/Arith.ML | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Arith.ML Tue Jul 27 22:03:24 1999 +0200 +++ b/src/HOL/Arith.ML Tue Jul 27 22:04:30 1999 +0200 @@ -1107,7 +1107,7 @@ qed "diff_less"; -(** (Anti)Monotonicity of subtraction -- by Stefan Merz **) +(** (Anti)Monotonicity of subtraction -- by Stephan Merz **) (* Monotonicity of subtraction in first argument *) Goal "m <= (n::nat) ==> (m-l) <= (n-l)";