src/HOL/ex/Dedekind_Real.thy
changeset 37388 793618618f78
parent 36794 f736a853864f
child 37765 26bdfb7b680b
     1.1 --- a/src/HOL/ex/Dedekind_Real.thy	Tue Jun 08 16:37:19 2010 +0200
     1.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Tue Jun 08 16:37:22 2010 +0200
     1.3 @@ -2006,7 +2006,7 @@
     1.4  qed
     1.5  
     1.6  text {*
     1.7 -  There must be other proofs, e.g. @{text "Suc"} of the largest
     1.8 +  There must be other proofs, e.g. @{text Suc} of the largest
     1.9    integer in the cut representing @{text "x"}.
    1.10  *}
    1.11