diff -r 119b9f7e34c0 -r 9b9723930a02 LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Wed Sep 21 19:57:17 2011 +0200 +++ b/LMCS-Paper/Paper.thy Thu Sep 22 07:41:48 2011 +0900 @@ -2382,7 +2382,7 @@ holds. This allows us to use the implication from the strong cases lemma, and we are done. - Conseqently, we can discharge all proof-obligations about having covered all + Consequently, we can discharge all proof-obligations about having covered all cases. This completes the proof establishing that the weak induction principles imply the strong induction principles. These strong induction principles have proved already to be very useful in practice, particularly for proving properties about