diff -r abc7f90188af -r 8def50824320 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Tue Apr 07 17:04:39 2009 +0100 +++ b/ProgTutorial/FirstSteps.thy Tue Apr 07 23:59:39 2009 +0100 @@ -919,7 +919,7 @@ "Const (\"op =\", \"int \ int \ bool\") $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"} - (FIXME: readmore about types) + (FIXME: a readmore about types) *} @@ -1114,7 +1114,7 @@ (FIXME: handy functions working on theorems, like @{ML ObjectLogic.rulify} and so on) - (FIXME how to add case-names to goal states - maybe in the + (FIXME: how to add case-names to goal states - maybe in the next section) *}