changeset 62847 | 1bd1d8492931 |
parent 62829 | 4141c2a8458b |
child 63669 | 256fc20716f2 |
--- a/src/Doc/System/Environment.thy Mon Apr 04 15:53:56 2016 +0200 +++ b/src/Doc/System/Environment.thy Mon Apr 04 16:14:22 2016 +0200 @@ -395,8 +395,8 @@ The user is connected to the raw ML toplevel loop: this is neither Isabelle/Isar nor Isabelle/ML within the usual formal context. The most - relevant ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML - use_thys}. + relevant ML commands at this stage are @{ML use} (for ML files) and + @{ML use_thy} (for theory files). \<close>