# HG changeset patch
# User wenzelm
# Date 1453244808 -3600
# Node ID aed720a91f2f4adbcd123f6161da40bd59d0c53c
# Parent  ca68dc26fbb674015134c80e16a34732ef2725c6
tuned;

diff -r ca68dc26fbb6 -r aed720a91f2f src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Tue Jan 19 14:00:47 2016 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Wed Jan 20 00:06:48 2016 +0100
@@ -1115,7 +1115,7 @@
   local checks of the given type and its representing set.
 
   Recent clarification of overloading in the HOL logic proper @{cite
-  "Kuncar-Popescu:2015"} demonstrate how the dissimilar concepts of constant
+  "Kuncar-Popescu:2015"} demonstrates how the dissimilar concepts of constant
   definitions versus type definitions may be understood uniformly. This
   requires an interpretation of Isabelle/HOL that substantially reforms the
   set-theoretic model of A. Pitts @{cite "pitts93"}, by taking a schematic