| changeset 39846 | cb6634eb8926 |
| parent 39839 | 08f59175e541 |
| child 39857 | ea93e088398d |
--- a/doc-src/IsarImplementation/Thy/Prelim.thy Wed Oct 13 11:15:15 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy Wed Oct 13 13:05:23 2010 +0100 @@ -1081,8 +1081,8 @@ ML {* Binding.pos_of @{binding here} *} -text {* \medskip That position can be also printed in a message as - follows. *} +text {* \medskip\noindent That position can be also printed in a + message as follows. *} ML_command {* writeln