--- a/src/HOL/Nat.thy Sat Feb 19 18:44:34 2005 +0100 +++ b/src/HOL/Nat.thy Mon Feb 21 15:04:10 2005 +0100 @@ -1022,4 +1022,5 @@ apply (fastsimp dest: mult_less_mono2) done + end