diff -r af3e6576e680 -r f05b7d6ec592 src/Doc/Isar_Ref/Misc.thy --- a/src/Doc/Isar_Ref/Misc.thy Tue Apr 15 00:14:57 2014 +0200 +++ b/src/Doc/Isar_Ref/Misc.thy Tue Apr 15 00:21:31 2014 +0200 @@ -133,7 +133,7 @@ \item @{command "pwd"} prints the current working directory. - \item @{command "use_thy"}~@{text A} preload theory @{text A}. + \item @{command "use_thy"}~@{text A} preloads theory @{text A}. These system commands are scarcely used when working interactively, since loading of theories is done automatically as required.