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"}