changeset 62551 | df62e1ab7d88 |
parent 62509 | 13d6948e4b12 |
child 62559 | 83e815849a91 |
--- a/src/Doc/System/Misc.thy Mon Mar 07 21:33:41 2016 +0100 +++ b/src/Doc/System/Misc.thy Mon Mar 07 21:53:21 2016 +0100 @@ -94,8 +94,7 @@ Interaction works via the raw ML toplevel loop: this is neither Isabelle/Isar nor Isabelle/ML within the usual formal context. Some useful - ML commands at this stage are @{ML cd}, @{ML pwd}, @{ML use}, @{ML use_thy}, - @{ML use_thys}. + ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML use_thys}. \<close>