ProgTutorial/Advanced.thy
changeset 471 f65b9f14d5de
parent 463 b6fc4d1b75d0
child 475 25371f74c768
--- a/ProgTutorial/Advanced.thy	Tue Jun 28 08:44:34 2011 +0100
+++ b/ProgTutorial/Advanced.thy	Tue Jun 28 09:22:00 2011 +0100
@@ -287,7 +287,6 @@
 *}
 
 text {* 
-  @{ML_ind "Binding.str_of"} returns the string with markup;
   @{ML_ind "Binding.name_of"} returns the string without markup
 
   @{ML_ind "Binding.conceal"}