doc-src/Locales/Locales/Examples.thy
changeset 33838 a3166a169793
parent 32984 2ef1adff7eee
child 36176 3fe7e97ccca8
--- a/doc-src/Locales/Locales/Examples.thy	Sat Nov 21 17:39:54 2009 +0100
+++ b/doc-src/Locales/Locales/Examples.thy	Sat Nov 21 18:25:53 2009 +0100
@@ -26,7 +26,7 @@
 \[
   @{text "\<And>x\<^sub>1\<dots>x\<^sub>n. \<lbrakk> A\<^sub>1; \<dots> ;A\<^sub>m \<rbrakk> \<Longrightarrow> \<dots>"}
 \]
-  where variables~@{text "x\<^sub>1"}, \ldots,~@{text "x\<^sub>n"} are called
+  where the variables~@{text "x\<^sub>1"}, \ldots,~@{text "x\<^sub>n"} are called
   \emph{parameters} and the premises $@{text "A\<^sub>1"}, \ldots,~@{text
   "A\<^sub>m"}$ \emph{assumptions}.  A formula~@{text "C"}
   is a \emph{theorem} in the context if it is a conclusion