# HG changeset patch
# User wenzelm
# Date 1432300429 -7200
# Node ID 1f9e08394d465fd1d208be83ac27127ef3b13a53
# Parent  9e8d0f8e552b46b592ae90cf1b4be93b078eef99
tuned;

diff -r 9e8d0f8e552b -r 1f9e08394d46 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Fri May 22 15:10:35 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Fri May 22 15:13:49 2015 +0200
@@ -178,7 +178,7 @@
   accesses to the local scope, as determined by the enclosing @{command
   "context"}~@{keyword "begin"}~\dots~@{command "end"} block. Outside its
   scope, a @{keyword "private"} name is inaccessible, and a @{keyword
-  "qualified"} name is only accessible with additional qualification.
+  "qualified"} name is only accessible with some qualification.
 
   Neither a global @{command theory} nor a @{command locale} target provides
   a local scope by itself: an extra unnamed context is required to use
@@ -1541,7 +1541,7 @@
 
   \item @{command "hide_class"}~@{text names} fully removes class
   declarations from a given name space; with the @{text "(open)"}
-  option, only the base name is hidden.
+  option, only the unqualified base name is hidden.
 
   Note that hiding name space accesses has no impact on logical
   declarations --- they remain valid internally.  Entities that are no