# HG changeset patch
# User kleing
# Date 1307362314 -7200
# Node ID 04aaac80183f7093aee97106d94e7c691ea3552b
# Parent  f4f27123daef616bf6c267b9d1e48752d356e3ad
fixed typo

diff -r f4f27123daef -r 04aaac80183f src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Sun Jun 05 15:00:52 2011 +0200
+++ b/src/HOL/SetInterval.thy	Mon Jun 06 14:11:54 2011 +0200
@@ -348,7 +348,7 @@
 lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
 by (simp add: lessThan_def less_Suc_eq, blast)
 
-text {* The following proof is convinient in induction proofs where
+text {* The following proof is convenient in induction proofs where
 new elements get indices at the beginning. So it is used to transform
 @{term "{..<Suc n}"} to @{term "0::nat"} and @{term "{..< n}"}. *}