src/Doc/System/Misc.thy
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>