ProgTutorial/FirstSteps.thy
changeset 351 f118240ab44a
parent 350 364fffa80794
child 354 544c149005cf
--- a/ProgTutorial/FirstSteps.thy	Sun Oct 18 08:44:39 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sun Oct 18 21:22:44 2009 +0200
@@ -822,8 +822,8 @@
   @{ML_file "Pure/General/binding.ML"}.
   \end{readmore}
 
-  \footnote{\bf FIXME give a better example why bindings are important; maybe
-  give a pointer to \isacommand{local\_setup}; if not, then explain
+  \footnote{\bf FIXME give a better example why bindings are important}
+  \footnote{\bf FIXME give a pointer to \isacommand{local\_setup}; if not, then explain
   why @{ML snd} is needed.}
   \footnote{\bf FIXME: There should probably a separate section on binding, long-names
   and sign.}