Locales: new element constrains, parameter renaming with syntax,
authorballarin
Wed Jun 01 12:30:49 2005 +0200 (2005-06-01)
changeset 16168adb83939177f
parent 16167 b2e4c4058b71
child 16169 b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
experimental command instantiate withdrawn.
NEWS
doc-src/IsarRef/generic.tex
doc-src/Locales/IsaMakefile
doc-src/Locales/Locales/Locales.thy
doc-src/Locales/Locales/document/root.bib
doc-src/Locales/Makefile
doc-src/Locales/locales.tex
doc-src/isar.sty
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/FOL/IsaMakefile
src/FOL/ex/LocaleInst.thy
src/FOL/ex/LocaleTest.thy
src/FOL/ex/ROOT.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/NEWS	Wed Jun 01 10:52:17 2005 +0200
     1.2 +++ b/NEWS	Wed Jun 01 12:30:49 2005 +0200
     1.3 @@ -141,8 +141,11 @@
     1.4    - Fixed parameter management in theorem generation for goals with "includes".
     1.5      INCOMPATIBILITY: rarely, the generated theorem statement is different.
     1.6  
     1.7 -* Locales: locale expressions permit optional mixfix redeclaration for
     1.8 -  renamed parameters.
     1.9 +* Locales: new context element "constrains" for adding type constraints
    1.10 +  to parameters.
    1.11 +
    1.12 +* Locales: context expressions permit optional syntax redeclaration when
    1.13 +  renaming parameters.
    1.14  
    1.15  * Locales: new commands for the interpretation of locale expressions
    1.16    in theories (interpretation) and proof contexts (interpret).  These take an
    1.17 @@ -155,6 +158,9 @@
    1.18    Use print_interps to inspect active interpretations of a particular locale.
    1.19    For details, see the Isar Reference manual.
    1.20  
    1.21 +* Locales: INCOMPATIBILITY: experimental command "instantiate" has
    1.22 +  been withdrawn.  Use "interpret" instead.
    1.23 +
    1.24  * Locales: proper static binding of attribute syntax -- i.e. types /
    1.25    terms / facts mentioned as arguments are always those of the locale
    1.26    definition context, independently of the context of later
     2.1 --- a/doc-src/IsarRef/generic.tex	Wed Jun 01 10:52:17 2005 +0200
     2.2 +++ b/doc-src/IsarRef/generic.tex	Wed Jun 01 12:30:49 2005 +0200
     2.3 @@ -122,10 +122,12 @@
     2.4    contextexpr: nameref | '(' contextexpr ')' |
     2.5    (contextexpr (name mixfix? +)) | (contextexpr + '+')
     2.6    ;
     2.7 -  contextelem: fixes | assumes | defines | notes | includes
     2.8 +  contextelem: fixes | constrains | assumes | defines | notes | includes
     2.9    ;
    2.10    fixes: 'fixes' (name ('::' type)? structmixfix? + 'and')
    2.11    ;
    2.12 +  constrains: 'constrains' (name '::' type + 'and')
    2.13 +  ;
    2.14    assumes: 'assumes' (thmdecl? props + 'and')
    2.15    ;
    2.16    defines: 'defines' (thmdecl? prop proppat? + 'and')
    2.17 @@ -168,6 +170,9 @@
    2.18      declaration ``$(structure)$'' means that $x$ may be referenced
    2.19      implicitly in this context.
    2.20  
    2.21 +  \item [$\CONSTRAINS{~x::\tau}$] introduces a type constraint $\tau$
    2.22 +    on the local parameter $x$.
    2.23 +
    2.24    \item [$\ASSUMES{a}{\vec\phi}$] introduces local premises, similar to
    2.25      $\ASSUMENAME$ within a proof (cf.\ \S\ref{sec:proof-context}).
    2.26  
    2.27 @@ -305,6 +310,15 @@
    2.28    account when choosing attributes for local theorems.
    2.29  \end{warn}
    2.30  
    2.31 +\begin{warn}
    2.32 +  An interpretation may subsume previous interpretations.  A warning
    2.33 +  is issued, since it is likely that these could have been generalized
    2.34 +  in the first place.  The locale package does not attempt to remove
    2.35 +  subsumed interpretations.  This situation is normally harmless, but
    2.36 +  note that $blast$ gets confused by the presence of multiple axclass
    2.37 +  instances a rule.
    2.38 +\end{warn}
    2.39 +
    2.40  
    2.41  \section{Derived proof schemes}
    2.42  
     3.1 --- a/doc-src/Locales/IsaMakefile	Wed Jun 01 10:52:17 2005 +0200
     3.2 +++ b/doc-src/Locales/IsaMakefile	Wed Jun 01 12:30:49 2005 +0200
     3.3 @@ -13,7 +13,7 @@
     3.4  SRC = $(ISABELLE_HOME)/src
     3.5  OUT = $(ISABELLE_OUTPUT)
     3.6  LOG = $(OUT)/log
     3.7 -USEDIR = $(ISATOOL) usedir -i true -d "" -D generated
     3.8 +USEDIR = $(ISATOOL) usedir -i true -d "" -H false -D generated
     3.9  
    3.10  
    3.11  ## Locales
    3.12 @@ -23,7 +23,7 @@
    3.13  HOL:
    3.14  	@cd $(SRC)/HOL; $(ISATOOL) make HOL
    3.15  
    3.16 -$(LOG)/HOL-Locales.gz: $(OUT)/HOL Locales/ROOT.ML Locales/Locales.thy
    3.17 +$(LOG)/HOL-Locales.gz: $(OUT)/HOL Locales/ROOT.ML Locales/Locales.thy Locales/document/root.tex Locales/document/root.bib
    3.18  	@$(USEDIR) $(OUT)/HOL Locales
    3.19  
    3.20  
     4.1 --- a/doc-src/Locales/Locales/Locales.thy	Wed Jun 01 10:52:17 2005 +0200
     4.2 +++ b/doc-src/Locales/Locales/Locales.thy	Wed Jun 01 12:30:49 2005 +0200
     4.3 @@ -14,6 +14,9 @@
     4.4  section {* Overview *}
     4.5  
     4.6  text {*
     4.7 +  The present text is based on~\cite{Ballarin2004a}.  It was updated
     4.8 +  for for Isabelle2005, but does not cover locale interpretation.
     4.9 +
    4.10    Locales are an extension of the Isabelle proof assistant.  They
    4.11    provide support for modular reasoning. Locales were initially
    4.12    developed by Kamm\"uller~\cite{Kammuller2000} to support reasoning
    4.13 @@ -129,9 +132,9 @@
    4.14    Figure~\ref{fig-grammar}.
    4.15    A key concept, introduced by Wenzel, is that
    4.16    locales are (internally) lists
    4.17 -  of \emph{context elements}.  There are four kinds, identified
    4.18 -  by the keywords \textbf{fixes}, \textbf{assumes}, \textbf{defines} and
    4.19 -  \textbf{notes}.
    4.20 +  of \emph{context elements}.  There are five kinds, identified
    4.21 +  by the keywords \textbf{fixes}, \textbf{constrains},
    4.22 +  \textbf{assumes}, \textbf{defines} and \textbf{notes}.
    4.23  
    4.24    \begin{figure}
    4.25    \hrule
    4.26 @@ -146,13 +149,15 @@
    4.27    & \textit{locale-expr1} ( ``\textbf{+}'' \textit{locale-expr1} )$^*$ \\
    4.28    \textit{locale-expr1} & ::=
    4.29    & ( \textit{qualified-name} $|$
    4.30 -    ``\textbf{(}'' \textit{locale-expr} ``\textbf{)}'' )
    4.31 -    ( \textit{name} $|$ ``\textbf{\_}'' )$^*$ \\
    4.32 +    ``\textbf{(}'' \textit{locale-expr} ``\textbf{)}'' ) \\
    4.33 +  & & ( \textit{name} [ \textit{mixfix} ] $|$ ``\textbf{\_}'' )$^*$ \\
    4.34  
    4.35    \textit{fixes} & ::=
    4.36    & \textit{name} [ ``\textbf{::}'' \textit{type} ]
    4.37      [ ``\textbf{(}'' \textbf{structure} ``\textbf{)}'' $|$
    4.38      \textit{mixfix} ] \\
    4.39 +  \textit{constrains} & ::=
    4.40 +  & \textit{name} ``\textbf{::}'' \textit{type} \\
    4.41    \textit{assumes} & ::=
    4.42    & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
    4.43    \textit{defines} & ::=
    4.44 @@ -164,11 +169,16 @@
    4.45    \textit{element} & ::=
    4.46    & \textbf{fixes} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ \\
    4.47    & |
    4.48 +  & \textbf{constrains} \textit{constrains}
    4.49 +    ( \textbf{and} \textit{constrains} )$^*$ \\
    4.50 +  & |
    4.51    & \textbf{assumes} \textit{assumes} ( \textbf{and} \textit{assumes} )$^*$ \\
    4.52    & |
    4.53    & \textbf{defines} \textit{defines} ( \textbf{and} \textit{defines} )$^*$ \\
    4.54    & |
    4.55    & \textbf{notes} \textit{notes} ( \textbf{and} \textit{notes} )$^*$ \\
    4.56 +  \textit{element1} & ::=
    4.57 +  & \textit{element} \\
    4.58    & | & \textbf{includes} \textit{locale-expr} \\
    4.59  
    4.60    \textit{locale} & ::=
    4.61 @@ -191,7 +201,7 @@
    4.62    & | & \textbf{declare} [ \textit{in-target} ] ( \textit{qualified-name}
    4.63      [ \textit{attribute} ] )$^+$ \\
    4.64    & | & \textit{theorem} \textit{proposition} \textit{proof} \\
    4.65 -  & | & \textit{theorem} \textit{element}$^*$
    4.66 +  & | & \textit{theorem} \textit{element1}$^*$
    4.67      \textbf{shows} \textit{proposition} \textit{proof} \\
    4.68    & | & \textbf{print\_locale} \textit{locale} \\
    4.69    & | & \textbf{print\_locales}
    4.70 @@ -210,8 +220,7 @@
    4.71    declaring a named locale, it is possible to \emph{import} another
    4.72    named locale, or indeed several ones by importing a locale
    4.73    expression.  The second part of the declaration, also optional,
    4.74 -  consists of a number of context element declarations.  Here, a fifth
    4.75 -  kind, \textbf{includes}, is available.
    4.76 +  consists of a number of context element declarations.
    4.77  
    4.78    A number of Isar commands have an additional, optional \emph{target}
    4.79    argument, which always refers to a named locale.  These commands
    4.80 @@ -226,7 +235,7 @@
    4.81    \textbf{theorem} (and related commands), theorems stored in the target
    4.82    can be used in the associated proof scripts.
    4.83  
    4.84 -  The Locales package permits a \emph{long goals format} for
    4.85 +  The Locales package provides a \emph{long goals format} for
    4.86    propositions stated with \textbf{theorem} (and friends).  While
    4.87    normally a goal is just a formula, a long goal is a list of context
    4.88    elements, followed by the keyword \textbf{shows}, followed by the
    4.89 @@ -286,15 +295,15 @@
    4.90  
    4.91  text {*
    4.92    The parameter @{term prod} has a
    4.93 -  syntax annotation allowing the infix ``@{text "\<cdot>"}'' in the
    4.94 +  syntax annotation enabling the infix ``@{text "\<cdot>"}'' in the
    4.95    assumption of associativity.  Parameters may have arbitrary mixfix
    4.96    syntax, like constants.  In the example, the type of @{term prod} is
    4.97    specified explicitly.  This is not necessary.  If no type is
    4.98    specified, a most general type is inferred simultaneously for all
    4.99    parameters, taking into account all assumptions (and type
   4.100    specifications of parameters, if present).%
   4.101 -\footnote{Type inference also takes into account definitions and
   4.102 -  import, as introduced later.}
   4.103 +\footnote{Type inference also takes into account type constraints,
   4.104 +  definitions and import, as introduced later.}
   4.105  
   4.106    Free variables in assumptions are implicitly universally quantified,
   4.107    unless they are parameters.  Hence the context defined by the locale
   4.108 @@ -587,8 +596,8 @@
   4.109    The expression is only well-formed if $n$ does not
   4.110    exceed the number of parameters of $e$.  Underscores denote
   4.111    parameters that are not renamed.
   4.112 -  Parameters whose names are changed lose mixfix syntax,
   4.113 -  and there is currently no way to re-equip them with such.
   4.114 +  Renaming by default removes mixfix syntax, but new syntax may be
   4.115 +  specified.
   4.116  \item[Merge.]
   4.117    The locale expression $e_1 + e_2$ denotes
   4.118    the locale obtained by merging the locales of $e_1$
   4.119 @@ -615,16 +624,16 @@
   4.120    specification of semigroup homomorphisms.
   4.121  *}
   4.122  
   4.123 -locale semi_hom = comm_semi sum + comm_semi +
   4.124 +locale semi_hom = comm_semi sum (infixl "\<oplus>" 65) + comm_semi +
   4.125    fixes hom
   4.126 -  assumes hom: "hom (sum x y) = hom x \<cdot> hom y"
   4.127 +  assumes hom: "hom (x \<oplus> y) = hom x \<cdot> hom y"
   4.128  
   4.129  text {*
   4.130    This locale defines a context with three parameters @{text "sum"},
   4.131 -  @{text "prod"} and @{text "hom"}.  Only the second parameter has
   4.132 -  mixfix syntax.  The first two are associative operations,
   4.133 -  the first of type @{typ "['a, 'a] \<Rightarrow> 'a"}, the second of
   4.134 -  type @{typ "['b, 'b] \<Rightarrow> 'b"}.  
   4.135 +  @{text "prod"} and @{text "hom"}.  The first two parameters have
   4.136 +  mixfix syntax.  They are associative operations,
   4.137 +  the first of type @{typeof [locale=semi_hom] prod}, the second of
   4.138 +  type @{typeof [locale=semi_hom] sum}.  
   4.139  
   4.140    How are facts that are imported via a locale expression identified?
   4.141    Facts are always introduced in a named locale (either in the
   4.142 @@ -643,12 +652,12 @@
   4.143    facts, though.
   4.144  *}
   4.145  
   4.146 -theorem (in semi_hom) "hom x \<cdot> (hom y \<cdot> hom z) = hom (sum x (sum y z))"
   4.147 +theorem (in semi_hom) "hom x \<cdot> (hom y \<cdot> hom z) = hom (x \<oplus> (y \<oplus> z))"
   4.148  proof -
   4.149    have "hom x \<cdot> (hom y \<cdot> hom z) = hom y \<cdot> (hom x \<cdot> hom z)"
   4.150      by (simp add: prod.lcomm)
   4.151 -  also have "\<dots> = hom (sum y (sum x z))" by (simp add: hom)
   4.152 -  also have "\<dots> = hom (sum x (sum y z))" by (simp add: sum.lcomm)
   4.153 +  also have "\<dots> = hom (y \<oplus> (x \<oplus> z))" by (simp add: hom)
   4.154 +  also have "\<dots> = hom (x \<oplus> (y \<oplus> z))" by (simp add: sum.lcomm)
   4.155    finally show ?thesis .
   4.156  qed
   4.157  
   4.158 @@ -822,15 +831,16 @@
   4.159    and the list of context elements
   4.160  \[
   4.161  \begin{array}{ll}
   4.162 -  \textbf{fixes} & @{text sum} :: @{typ [quotes] "['a, 'a] \<Rightarrow> 'a"} \\
   4.163 +  \textbf{fixes} & @{text sum} :: @{typ [quotes] "['a, 'a] \<Rightarrow> 'a"}
   4.164 +    ~(\textbf{infixl}~@{text [quotes] "\<oplus>"}~65) \\
   4.165    \textbf{assumes} & @{text [quotes] "semi sum"} \\
   4.166 -  \textbf{notes} & @{text sum.assoc}: @{text [quotes] "sum (sum ?x ?y) ?z
   4.167 +  \textbf{notes} & @{text sum.assoc}: @{text [quotes] "(?x \<oplus> ?y) \<oplus> ?z
   4.168      = sum ?x (sum ?y ?z)"} \\
   4.169    \textbf{assumes} & @{text [quotes] "comm_semi_axioms sum"} \\
   4.170 -  \textbf{notes} & @{text sum.comm}: @{text [quotes] "sum ?x ?y = sum
   4.171 -    ?y ?x"} \\
   4.172 -  \textbf{notes} & @{text sum.lcomm}: @{text [quotes] "sum ?x (sum ?y ?z)
   4.173 -    = sum ?y (sum ?x ?z)"}
   4.174 +  \textbf{notes} & @{text sum.comm}: @{text [quotes] "?x \<oplus> ?y = 
   4.175 +    ?y \<oplus> ?x"} \\
   4.176 +  \textbf{notes} & @{text sum.lcomm}: @{text [quotes] "?x \<oplus> (?y \<oplus> ?z)
   4.177 +    = ?y \<oplus> (?x \<oplus> ?z)"}
   4.178  \end{array}
   4.179  \]
   4.180  
   4.181 @@ -867,14 +877,15 @@
   4.182    Hence $\C(@{text "semi_hom"})$, shown below, is again well-formed.
   4.183  \[
   4.184  \begin{array}{ll}
   4.185 -  \textbf{fixes} & @{text sum} :: @{typ [quotes] "['a, 'a] \<Rightarrow> 'a"} \\
   4.186 +  \textbf{fixes} & @{text sum} :: @{typ [quotes] "['a, 'a] \<Rightarrow> 'a"}
   4.187 +    ~(\textbf{infixl}~@{text [quotes] "\<oplus>"}~65) \\
   4.188    \textbf{assumes} & @{text [quotes] "semi sum"} \\
   4.189 -  \textbf{notes} & @{text sum.assoc}: @{text [quotes] "sum (sum ?x ?y) ?z
   4.190 -    = sum ?x (sum ?y ?z)"} \\
   4.191 +  \textbf{notes} & @{text sum.assoc}: @{text [quotes] "(?x \<oplus> ?y) \<oplus> ?z
   4.192 +    = ?x \<oplus> (?y \<oplus> ?z)"} \\
   4.193    \textbf{assumes} & @{text [quotes] "comm_semi_axioms sum"} \\
   4.194 -  \textbf{notes} & @{text sum.comm}: @{text [quotes] "sum ?x ?y = sum ?y ?x"} \\
   4.195 -  \textbf{notes} & @{text sum.lcomm}: @{text [quotes] "sum ?x (sum ?y ?z)
   4.196 -    = sum ?y (sum ?x ?z)"} \\
   4.197 +  \textbf{notes} & @{text sum.comm}: @{text [quotes] "?x \<oplus> ?y = ?y \<oplus> ?x"} \\
   4.198 +  \textbf{notes} & @{text sum.lcomm}: @{text [quotes] "?x \<oplus> (?y \<oplus> ?z)
   4.199 +    = ?y \<oplus> (?x \<oplus> ?z)"} \\
   4.200    \textbf{fixes} & @{text prod} :: @{typ [quotes] "['b, 'b] \<Rightarrow> 'b"}
   4.201      ~(\textbf{infixl}~@{text [quotes] "\<cdot>"}~70) \\
   4.202    \textbf{assumes} & @{text [quotes] "semi prod"} \\
   4.203 @@ -887,7 +898,7 @@
   4.204    \textbf{fixes} & @{text hom} :: @{typ [quotes] "'a \<Rightarrow> 'b"} \\
   4.205    \textbf{assumes} & @{text [quotes] "semi_hom_axioms sum"} \\
   4.206    \textbf{notes} & @{text "sum_prod_hom.hom"}:
   4.207 -    @{text "hom (sum x y) = hom x \<cdot> hom y"}
   4.208 +    @{text "hom (x \<oplus> y) = hom x \<cdot> hom y"}
   4.209  \end{array}
   4.210  \]
   4.211  
   4.212 @@ -959,11 +970,17 @@
   4.213    particular mixfix syntax is required.
   4.214    Its definition is
   4.215  \begin{center}
   4.216 -  \textbf{locale} \textit{var} = \textbf{fixes} @{text "x_"}
   4.217 +  \textbf{locale} @{text var} = \textbf{fixes} @{text "x_"}
   4.218  \end{center}
   4.219 -   The use of the internal variable @{text "x_"}
   4.220 +  The use of the internal variable @{text "x_"}
   4.221    enforces that the parameter is renamed before being used, because
   4.222 -  internal variables may not occur in the input syntax.
   4.223 +  internal variables may not occur in the input syntax.  Using
   4.224 +  @{text var}, the locale @{text magma} could have been replaced by
   4.225 +  the locale expression
   4.226 +\begin{center}
   4.227 +  @{text var} @{text prod} (\textbf{infixl} @{text [quotes] \<cdot>} 70)
   4.228 +\end{center}
   4.229 +  in the above locale declarations.
   4.230  *}
   4.231  
   4.232  subsection {* Includes *}
   4.233 @@ -971,20 +988,7 @@
   4.234  text {*
   4.235  \label{sec-includes}
   4.236    The context element \textbf{includes} takes a locale expression $e$
   4.237 -  as argument.  It can occur at any point in a locale declaration, and
   4.238 -  it adds $\C(e)$ to the current context.
   4.239 -
   4.240 -  If \textbf{includes} $e$ appears as context element in the
   4.241 -  declaration of a named locale $l$, the included context is only
   4.242 -  visible in subsequent context elements, but it is not propagated to
   4.243 -  $l$.  That is, if $l$ is later used as a target, context elements
   4.244 -  from $\C(e)$ are not added to the context.  Although it is
   4.245 -  conceivable that this mechanism could be used to add only selected
   4.246 -  facts from $e$ to $l$ (with \textbf{notes} elements following
   4.247 -  \textbf{includes} $e$), currently no useful applications of this are
   4.248 -  known.
   4.249 -
   4.250 -  The more common use of \textbf{includes} $e$ is in long goals, where it
   4.251 +  as argument.  It can only occur in long goals, where it
   4.252    adds, like a target, locale context to the proof context.  Unlike
   4.253    with targets, the proved theorem is not stored
   4.254    in the locale.  Instead, it is exported immediately.
   4.255 @@ -1049,13 +1053,10 @@
   4.256    effective in the context of a locale, and only if the first argument
   4.257    is a
   4.258    \emph{structural} parameter --- that is, a parameter with annotation
   4.259 -  \textbf{(structure)}.  The token has the effect of replacing the
   4.260 -  parameter with a subscripted number, the index of the structural
   4.261 -  parameter in the locale.  This replacement takes place both for
   4.262 -  printing and
   4.263 -  parsing.  Subscripted $1$ for the first structural
   4.264 -  parameter may be omitted, as in this specification of semigroups with
   4.265 -  structures:
   4.266 +  \textbf{(structure)}.  The token has the effect of subscripting the
   4.267 +  parameter --- by bracketing it between \verb.\<^bsub>. and  \verb.\<^esub>..
   4.268 +  Additionally, the subscript of the first structural parameter may be
   4.269 +  omitted, as in this specification of semigroups with structures:
   4.270  *}
   4.271  
   4.272  locale comm_semi' =
   4.273 @@ -1063,22 +1064,20 @@
   4.274    assumes assoc: "(x \<star> y) \<star> z = x \<star> (y \<star> z)" and comm: "x \<star> y = y \<star> x"
   4.275  
   4.276  text {*
   4.277 -  Here @{text "x \<star> y"} is equivalent to @{text "x \<star>\<^sub>1 y"} and
   4.278 -  abbreviates @{term "s_op G x y"}.  A specification of homomorphisms
   4.279 +  Here @{text "x \<star> y"} is equivalent to @{text "x \<star>\<^bsub>G\<^esub> y"} and
   4.280 +  abbreviates @{text "s_op G x y"}.  A specification of homomorphisms
   4.281    requires a second structural parameter.
   4.282  *}
   4.283  
   4.284  locale semi'_hom = comm_semi' + comm_semi' H +
   4.285    fixes hom
   4.286 -  assumes hom: "hom (x \<star> y) = hom x \<star>\<^sub>2 hom y"
   4.287 +  assumes hom: "hom (x \<star> y) = hom x \<star>\<^bsub>H\<^esub> hom y"
   4.288  
   4.289  text {*
   4.290    The parameter @{text H} is defined in the second \textbf{fixes}
   4.291 -  element of $\C(@{term "semi'_comm"})$. Hence @{text "\<star>\<^sub>2"}
   4.292 -  abbreviates @{term "s_op H x y"}.  The same construction can be done
   4.293 -  with records instead of an \textit{ad-hoc} type.  In general, the
   4.294 -  $i$th structural parameter is addressed by index $i$.  Only the
   4.295 -  index $1$ may be omitted.  *}
   4.296 +  element of $\C(@{term "semi'_comm"})$. Hence @{text "\<star>\<^bsub>H\<^esub>"}
   4.297 +  abbreviates @{text "s_op H x y"}.  The same construction can be done
   4.298 +  with records instead of an \textit{ad-hoc} type.  *}
   4.299  
   4.300  record 'a semi = prod :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<bullet>\<index>" 70)
   4.301  
   4.302 @@ -1119,7 +1118,7 @@
   4.303  section {* Conclusions and Outlook *}
   4.304  
   4.305  text {*
   4.306 -  Locales provide a simple means of modular reasoning.  They allow to
   4.307 +  Locales provide a simple means of modular reasoning.  They enable to
   4.308    abbreviate frequently occurring context statements and maintain facts
   4.309    valid in these contexts.  Importantly, using structures, they allow syntax to be
   4.310    effective only in certain contexts, and thus to mimic common
   4.311 @@ -1157,7 +1156,7 @@
   4.312    A detailed comparison of locales with module systems in type theory
   4.313    has not been undertaken yet, but could be beneficial.  For example,
   4.314    a module system for Coq has recently been presented by Chrzaszcz
   4.315 -  \cite{Chrzaszcz2003}.  While the
   4.316 +  \cite{Chrzaszcz2003,Chrzaszcz2004}.  While the
   4.317    latter usually constitute extensions of the calculus, locales are
   4.318    a rather thin layer that does not change Isabelle's meta logic.
   4.319    Locales mainly manage specifications and facts.  Functors, like
     5.1 --- a/doc-src/Locales/Locales/document/root.bib	Wed Jun 01 10:52:17 2005 +0200
     5.2 +++ b/doc-src/Locales/Locales/document/root.bib	Wed Jun 01 12:30:49 2005 +0200
     5.3 @@ -32,8 +32,7 @@
     5.4    title = "Types for Proofs and Programs: International Workshop, {TYPES} '98, {Kloster Irsee, Germany, March 27--31, 1998}, Selected Papers",
     5.5    booktitle = "TYPES '98",
     5.6    publisher = "Springer",
     5.7 -  series = "LNCS",
     5.8 -  number = 1657,
     5.9 +  series = "LNCS 1657",
    5.10    year = 1999
    5.11  }
    5.12  % CADE-17
    5.13 @@ -51,8 +50,7 @@
    5.14    title = "17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17--20, 2000: Proceedings",
    5.15    booktitle = "CADE 17",
    5.16    publisher = "Springer",
    5.17 -  series = "LNCS",
    5.18 -  number = 1831,
    5.19 +  series = "LNCS 1831",
    5.20    year = 2000
    5.21  }
    5.22  
    5.23 @@ -60,8 +58,7 @@
    5.24    author = "Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel",
    5.25    title = "{Isabelle/HOL}: A Proof Assistant for Higher-Order Logic",
    5.26    publisher = "Springer",
    5.27 -  series = "LNCS",
    5.28 -  number = 2283,
    5.29 +  series = "LNCS 2283",
    5.30    year = 2002,
    5.31    available = { CB }
    5.32  }
    5.33 @@ -80,8 +77,7 @@
    5.34    title = "Types for Proofs and Programs (TYPES 2002)",
    5.35    booktitle = "TYPES 2002",
    5.36    publisher = "Springer",
    5.37 -  series = "LNCS",
    5.38 -  number = 2646,
    5.39 +  series = "LNCS 2646",
    5.40    year = 2003
    5.41  }
    5.42  
    5.43 @@ -110,7 +106,7 @@
    5.44  % TPHOLs 2003
    5.45  
    5.46  @inproceedings{Chrzaszcz2003,
    5.47 -  author = "Jacek Chrzaszcz",
    5.48 +  author = "Jacek Chrz{\c{a}}szcz",
    5.49    title = "Implementing Modules in the {Coq} System",
    5.50    pages = "270--286",
    5.51    crossref = "BasinWolff2003",
    5.52 @@ -122,8 +118,7 @@
    5.53    title = "Theorem proving in higher order logics: 16th International Conference, TPHOLs 2003, Rome, Italy, September 2003: proceedings",
    5.54    booktitle = "TPHOLs 2003",
    5.55    publisher = "Springer",
    5.56 -  series = "LNCS",
    5.57 -  number = 2758,
    5.58 +  series = "LNCS 2758",
    5.59    year = 2003
    5.60  }
    5.61  
    5.62 @@ -148,7 +143,31 @@
    5.63    title     = {Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Berlin, Germany, March 25 -- April 2, 2000, Proceedings},
    5.64    booktitle     = "TACAS 2000",
    5.65    publisher = {Springer},
    5.66 -  series    = {LNCS},
    5.67 -  number    = {1785},
    5.68 +  series    = {LNCS 1785},
    5.69    year      = {2000},
    5.70 -}
    5.71 \ No newline at end of file
    5.72 +}
    5.73 +
    5.74 +% TYPES 2004
    5.75 +
    5.76 +@inproceedings{Ballarin2004a,
    5.77 +  author = "Clemens Ballarin",
    5.78 +  title = "Locales and Locale Expressions in {Isabelle/Isar}",
    5.79 +  pages = "34--50",
    5.80 +  crossref = "BerardiEtAl2004"
    5.81 +}
    5.82 +
    5.83 +@inproceedings{Chrzaszcz2004,
    5.84 +  author = "Jacek Chrz{\c{a}}szcz",
    5.85 +  title = "Modules in {Coq} Are and Will Be Correct",
    5.86 +  pages = "130--136",
    5.87 +  crossref = "BerardiEtAl2004",
    5.88 +  available = { CB }
    5.89 +}
    5.90 +@proceedings{BerardiEtAl2004,
    5.91 +  editor = "Stefano Berardi and Mario Coppo and Ferruccio Damiani",
    5.92 +  title = "Types for Proofs and Programs, TYPES 2003, Torino, Italy",
    5.93 +  booktitle = "Types for Proofs and Programs, TYPES 2003, Torino, Italy",
    5.94 +  publisher = "Springer",
    5.95 +  series = "LNCS 3085",
    5.96 +  year = 2004
    5.97 +}
     6.1 --- a/doc-src/Locales/Makefile	Wed Jun 01 10:52:17 2005 +0200
     6.2 +++ b/doc-src/Locales/Makefile	Wed Jun 01 12:30:49 2005 +0200
     6.3 @@ -16,7 +16,7 @@
     6.4  
     6.5  NAME = locales
     6.6  
     6.7 -FILES = locales.tex Locales/generated/root.bib \
     6.8 +FILES = Locales/generated/root.tex Locales/generated/root.bib \
     6.9    Locales/generated/session.tex Locales/generated/Locales.tex \
    6.10    Locales/generated/isabelle.sty Locales/generated/isabellesym.sty \
    6.11    Locales/generated/pdfsetup.sty 
    6.12 @@ -24,17 +24,19 @@
    6.13  dvi: $(NAME).dvi
    6.14  
    6.15  $(NAME).dvi: $(FILES)
    6.16 -	env TEXINPUTS=$(TEXPATH) $(LATEX) $(NAME)
    6.17 -	env BIBINPUTS=$(TEXPATH) $(BIBTEX) $(NAME)
    6.18 -	env TEXINPUTS=$(TEXPATH) $(LATEX) $(NAME)
    6.19 -	env TEXINPUTS=$(TEXPATH) $(LATEX) $(NAME)
    6.20 -	env TEXINPUTS=$(TEXPATH) $(LATEX) $(NAME)
    6.21 +	env TEXINPUTS=$(TEXPATH) $(LATEX) root
    6.22 +	env BIBINPUTS=$(TEXPATH) $(BIBTEX) root
    6.23 +	env TEXINPUTS=$(TEXPATH) $(LATEX) root
    6.24 +	env TEXINPUTS=$(TEXPATH) $(LATEX) root
    6.25 +	env TEXINPUTS=$(TEXPATH) $(LATEX) root
    6.26 +	mv root.dvi $(NAME).dvi
    6.27  
    6.28  pdf: $(NAME).pdf
    6.29  
    6.30  $(NAME).pdf: $(FILES)
    6.31 -	env TEXINPUTS=$(TEXPATH) $(PDFLATEX) $(NAME)
    6.32 -	env BIBINPUTS=$(TEXPATH) $(BIBTEX) $(NAME)
    6.33 -	env TEXINPUTS=$(TEXPATH) $(PDFLATEX) $(NAME)
    6.34 -	env TEXINPUTS=$(TEXPATH) $(PDFLATEX) $(NAME)
    6.35 -	env TEXINPUTS=$(TEXPATH) $(PDFLATEX) $(NAME)
    6.36 +	env TEXINPUTS=$(TEXPATH) $(PDFLATEX) root
    6.37 +	env BIBINPUTS=$(TEXPATH) $(BIBTEX) root
    6.38 +	env TEXINPUTS=$(TEXPATH) $(PDFLATEX) root
    6.39 +	env TEXINPUTS=$(TEXPATH) $(PDFLATEX) root
    6.40 +	env TEXINPUTS=$(TEXPATH) $(PDFLATEX) root
    6.41 +	mv root.pdf $(NAME).pdf
     7.1 --- a/doc-src/Locales/locales.tex	Wed Jun 01 10:52:17 2005 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,48 +0,0 @@
     7.4 -\documentclass[leqno]{article}
     7.5 -\usepackage{isabelle,isabellesym}
     7.6 -
     7.7 -\usepackage{amsmath}
     7.8 -\usepackage{amssymb}
     7.9 -\usepackage{array}
    7.10 -
    7.11 -% this should be the last package used
    7.12 -\usepackage{pdfsetup}
    7.13 -
    7.14 -\urlstyle{rm}
    7.15 -\isabellestyle{tt}
    7.16 -%\renewcommand{\isacharunderscore}{\_}%
    7.17 -% the latter is not necessary with \isabellestyle{tt}
    7.18 -
    7.19 -\begin{document}
    7.20 -
    7.21 -\title{Locales and Locale Expressions in Isabelle/Isar}
    7.22 -\author{Clemens Ballarin \\
    7.23 -  Fakult\"at f\"ur Informatik \\ Technische Universit\"at M\"unchen \\
    7.24 -  85748 Garching, Germany \\
    7.25 -  ballarin@in.tum.de}
    7.26 -\date{}
    7.27 -
    7.28 -\maketitle
    7.29 -
    7.30 -\begin{abstract}
    7.31 -  Locales provide a module system for the Isabelle proof assistant.
    7.32 -  Recently, locales have been ported to the new Isar format for
    7.33 -  structured proofs.  At the same time, they have been extended by
    7.34 -  locale expressions, a language for composing locale specifications,
    7.35 -  and by structures, which provide syntax for algebraic structures.
    7.36 -  The present paper presents both and is suitable as a tutorial to
    7.37 -  locales in Isar, because it covers both basics and recent
    7.38 -  extensions, and contains many examples.
    7.39 -\end{abstract}
    7.40 -
    7.41 -%\tableofcontents
    7.42 -
    7.43 -\parindent 0pt\parskip 0.5ex
    7.44 -
    7.45 -% include generated text of all theories
    7.46 -\input{session}
    7.47 -
    7.48 -\bibliographystyle{plain}
    7.49 -\bibliography{root}
    7.50 -
    7.51 -\end{document}
     8.1 --- a/doc-src/isar.sty	Wed Jun 01 10:52:17 2005 +0200
     8.2 +++ b/doc-src/isar.sty	Wed Jun 01 12:30:49 2005 +0200
     8.3 @@ -42,6 +42,7 @@
     8.4  \newcommand{\WITHNAME}{\isarkeyword{with}}
     8.5  \newcommand{\USINGNAME}{\isarkeyword{using}}
     8.6  \newcommand{\FIXESNAME}{\isarkeyword{fixes}}
     8.7 +\newcommand{\CONSTRAINSNAME}{\isarkeyword{constrains}}
     8.8  \newcommand{\ASSUMESNAME}{\isarkeyword{assumes}}
     8.9  \newcommand{\DEFINESNAME}{\isarkeyword{defines}}
    8.10  \newcommand{\NOTESNAME}{\isarkeyword{notes}}
    8.11 @@ -86,6 +87,7 @@
    8.12  \newcommand{\WITH}[1]{\WITHNAME~#1}
    8.13  \newcommand{\USING}[1]{\USINGNAME~#1}
    8.14  \newcommand{\FIXES}[1]{\FIXESNAME~#1}
    8.15 +\newcommand{\CONSTRAINS}[1]{\CONSTRAINSNAME~#1}
    8.16  \newcommand{\ASSUMES}[2]{\ASSUMESNAME\I@optname{#1}~#2}
    8.17  \newcommand{\DEFINES}[2]{\DEFINESNAME\I@optname{#1}~#2}
    8.18  \newcommand{\NOTES}[2]{\NOTESNAME~\ifthenelse{\equal{}{#1}}{}{#1=}#2}
     9.1 --- a/etc/isar-keywords-ZF.el	Wed Jun 01 10:52:17 2005 +0200
     9.2 +++ b/etc/isar-keywords-ZF.el	Wed Jun 01 12:30:49 2005 +0200
     9.3 @@ -73,7 +73,6 @@
     9.4      "inductive_cases"
     9.5      "init_toplevel"
     9.6      "instance"
     9.7 -    "instantiate"
     9.8      "interpret"
     9.9      "interpretation"
    9.10      "judgment"
    9.11 @@ -192,6 +191,7 @@
    9.12      "case_eqns"
    9.13      "con_defs"
    9.14      "concl"
    9.15 +    "constrains"
    9.16      "defines"
    9.17      "domains"
    9.18      "elimination"
    9.19 @@ -413,7 +413,6 @@
    9.20  
    9.21  (defconst isar-keywords-proof-decl
    9.22    '("also"
    9.23 -    "instantiate"
    9.24      "let"
    9.25      "moreover"
    9.26      "note"
    10.1 --- a/etc/isar-keywords.el	Wed Jun 01 10:52:17 2005 +0200
    10.2 +++ b/etc/isar-keywords.el	Wed Jun 01 12:30:49 2005 +0200
    10.3 @@ -76,7 +76,6 @@
    10.4      "inductive_cases"
    10.5      "init_toplevel"
    10.6      "instance"
    10.7 -    "instantiate"
    10.8      "interpret"
    10.9      "interpretation"
   10.10      "judgment"
   10.11 @@ -202,6 +201,7 @@
   10.12      "compose"
   10.13      "concl"
   10.14      "congs"
   10.15 +    "constrains"
   10.16      "defines"
   10.17      "distinct"
   10.18      "files"
   10.19 @@ -447,7 +447,6 @@
   10.20  
   10.21  (defconst isar-keywords-proof-decl
   10.22    '("also"
   10.23 -    "instantiate"
   10.24      "let"
   10.25      "moreover"
   10.26      "note"
    11.1 --- a/src/FOL/IsaMakefile	Wed Jun 01 10:52:17 2005 +0200
    11.2 +++ b/src/FOL/IsaMakefile	Wed Jun 01 12:30:49 2005 +0200
    11.3 @@ -47,7 +47,6 @@
    11.4  $(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy \
    11.5    ex/If.thy ex/IffOracle.ML ex/IffOracle.thy ex/List.ML ex/List.thy	\
    11.6    ex/LocaleTest.thy \
    11.7 -  ex/LocaleInst.thy \
    11.8    ex/Nat.ML ex/Nat.thy ex/Nat2.ML ex/Nat2.thy ex/Natural_Numbers.thy	\
    11.9    ex/Prolog.ML ex/Prolog.thy ex/ROOT.ML ex/Classical.thy ex/document/root.tex\
   11.10    ex/foundn.ML ex/Intuitionistic.thy ex/intro.ML ex/prop.ML ex/quant.ML
    12.1 --- a/src/FOL/ex/LocaleInst.thy	Wed Jun 01 10:52:17 2005 +0200
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,133 +0,0 @@
    12.4 -(*  Title:      FOL/ex/LocaleInst.thy
    12.5 -    ID:         $Id$
    12.6 -    Author:     Clemens Ballarin
    12.7 -    Copyright (c) 2004 by Clemens Ballarin
    12.8 -
    12.9 -Test of locale instantiation mechanism, also provides a few examples.
   12.10 -*)
   12.11 -
   12.12 -header {* Test of Locale instantiation *}
   12.13 -
   12.14 -theory LocaleInst = FOL:
   12.15 -
   12.16 -ML {* set show_hyps *}
   12.17 -
   12.18 -subsection {* Locale without assumptions *}
   12.19 -
   12.20 -locale L1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
   12.21 -
   12.22 -lemma "[| A; B |] ==> A & B"
   12.23 -proof -
   12.24 -  instantiate my: L1           txt {* No chained fact required. *}
   12.25 -  assume B and A               txt {* order reversed *}
   12.26 -  then show "A & B" ..         txt {* Applies @{thm my.rev_conjI}. *}
   12.27 -qed
   12.28 -
   12.29 -locale L11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]]
   12.30 -
   12.31 -lemma "[| A; B |] ==> A & B"
   12.32 -proof -
   12.33 -  instantiate [intro]: L11     txt {* Attribute supplied at instantiation. *}
   12.34 -  assume B and A
   12.35 -  then show "A & B" ..
   12.36 -qed
   12.37 -
   12.38 -subsection {* Simple locale with assumptions *}
   12.39 -
   12.40 -typedecl i
   12.41 -arities  i :: "term"
   12.42 -
   12.43 -consts bin :: "[i, i] => i" (infixl "#" 60)
   12.44 -
   12.45 -axioms i_assoc: "(x # y) # z = x # (y # z)"
   12.46 -  i_comm: "x # y = y # x"
   12.47 -
   12.48 -locale L2 =
   12.49 -  fixes OP (infixl "+" 60)
   12.50 -  assumes assoc: "(x + y) + z = x + (y + z)"
   12.51 -    and comm: "x + y = y + x"
   12.52 -
   12.53 -lemma (in L2) lcomm: "x + (y + z) = y + (x + z)"
   12.54 -proof -
   12.55 -  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
   12.56 -  also have "... = (y + x) + z" by (simp add: comm)
   12.57 -  also have "... = y + (x + z)" by (simp add: assoc)
   12.58 -  finally show ?thesis .
   12.59 -qed
   12.60 -
   12.61 -lemmas (in L2) AC = comm assoc lcomm
   12.62 -
   12.63 -lemma "(x::i) # y # z # w = y # x # w # z"
   12.64 -proof -
   12.65 -  have "L2 (op #)" by (rule L2.intro [of "op #", OF i_assoc i_comm])
   12.66 -  then instantiate my: L2
   12.67 -    txt {* Chained fact required to discharge assumptions of @{text L2}
   12.68 -      and instantiate parameters. *}
   12.69 -  show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
   12.70 -qed
   12.71 -
   12.72 -subsection {* Nested locale with assumptions *}
   12.73 -
   12.74 -locale L3 =
   12.75 -  fixes OP (infixl "+" 60)
   12.76 -  assumes assoc: "(x + y) + z = x + (y + z)"
   12.77 -
   12.78 -locale L4 = L3 +
   12.79 -  assumes comm: "x + y = y + x"
   12.80 -
   12.81 -lemma (in L4) lcomm: "x + (y + z) = y + (x + z)"
   12.82 -proof -
   12.83 -  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
   12.84 -  also have "... = (y + x) + z" by (simp add: comm)
   12.85 -  also have "... = y + (x + z)" by (simp add: assoc)
   12.86 -  finally show ?thesis .
   12.87 -qed
   12.88 -
   12.89 -lemmas (in L4) AC = comm assoc lcomm
   12.90 -
   12.91 -text {* Conceptually difficult locale:
   12.92 -   2nd context fragment contains facts with differing metahyps. *}
   12.93 -
   12.94 -lemma L4_intro:
   12.95 -  fixes OP (infixl "+" 60)
   12.96 -  assumes assoc: "!!x y z. (x + y) + z = x + (y + z)"
   12.97 -    and comm: "!!x y. x + y = y + x"
   12.98 -  shows "L4 (op+)"
   12.99 -    by (blast intro: L4.intro L3.intro assoc L4_axioms.intro comm)
  12.100 -
  12.101 -lemma "(x::i) # y # z # w = y # x # w # z"
  12.102 -proof -
  12.103 -  have "L4 (op #)" by (rule L4_intro [of "op #", OF i_assoc i_comm])
  12.104 -  then instantiate my: L4
  12.105 -  show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
  12.106 -qed
  12.107 -
  12.108 -subsection {* Locale with definition *}
  12.109 -
  12.110 -text {* This example is admittedly not very creative :-) *}
  12.111 -
  12.112 -locale L5 = L4 + var A +
  12.113 -  defines A_def: "A == True"
  12.114 -
  12.115 -lemma (in L5) lem: A
  12.116 -  by (unfold A_def) rule
  12.117 -
  12.118 -lemma "L5(op #) ==> True"
  12.119 -proof -
  12.120 -  assume "L5(op #)"
  12.121 -  then instantiate my: L5
  12.122 -  show ?thesis by (rule lem)  (* lem instantiated to True *)
  12.123 -qed
  12.124 -
  12.125 -subsection {* Instantiation in a context with target *}
  12.126 -
  12.127 -lemma (in L4)  (* Target might confuse instantiation command. *)
  12.128 -  fixes A (infixl "$" 60)
  12.129 -  assumes A: "L4(A)"
  12.130 -  shows "(x::i) $ y $ z $ w = y $ x $ w $ z"
  12.131 -proof -
  12.132 -  from A instantiate A: L4
  12.133 -  show ?thesis by (simp only: A.OP.AC)
  12.134 -qed
  12.135 -
  12.136 -end
    13.1 --- a/src/FOL/ex/LocaleTest.thy	Wed Jun 01 10:52:17 2005 +0200
    13.2 +++ b/src/FOL/ex/LocaleTest.thy	Wed Jun 01 12:30:49 2005 +0200
    13.3 @@ -13,16 +13,21 @@
    13.4  begin
    13.5  
    13.6  ML {* set quick_and_dirty *}    (* allow for thm command in batch mode *)
    13.7 -ML {* reset Toplevel.debug *}
    13.8 +ML {* set Toplevel.debug *}
    13.9  ML {* set show_hyps *}
   13.10  ML {* set show_sorts *}
   13.11  
   13.12  section {* Renaming with Syntax *}
   13.13  
   13.14 -locale S = var mult +
   13.15 +
   13.16 +locale (open) S = var mult +
   13.17    assumes "mult(x, y) = mult(y, x)"
   13.18 +(* Making this declaration (open) reveals a problem when mixing open and
   13.19 +   closed locales. *)
   13.20  
   13.21 -locale S' = S mult (infixl "**" 60)
   13.22 +print_locale S
   13.23 +
   13.24 +locale (open) S' = S mult (infixl "**" 60)
   13.25  
   13.26  print_locale S'
   13.27  
   13.28 @@ -32,17 +37,16 @@
   13.29  locale U = T mult (infixl "**" 60) + T add (infixl "++" 55) + var h +
   13.30    assumes hom: "h(x ** y) = h(x) ++ h(y)"
   13.31  
   13.32 -locale var' = fixes x :: "'a => 'b"
   13.33 +locale V = U _ add
   13.34  
   13.35 -(* doesn't work in FOL, but should in HOL *)
   13.36 -(* locale T' = var' mult (infixl "**" 60) *)
   13.37 +
   13.38 +section {* Constrains *}
   13.39  
   13.40 -locale V = U _ add
   13.41 -print_locale V
   13.42 -
   13.43 -locale T' = fixes mult assumes "mult(x, y) = mult(y, x)"
   13.44 -locale U' = T' mult + T' add + var h +
   13.45 -  assumes hom: "h(mult(x, y)) = add(h(x), h(y))"
   13.46 +locale Z = fixes a (structure)
   13.47 +locale Z' = Z +
   13.48 +  constrains a :: "'a => 'b"
   13.49 +  assumes "a (x :: 'a) = a (y)"
   13.50 +print_locale Z'
   13.51  
   13.52  
   13.53  section {* Interpretation *}
    14.1 --- a/src/FOL/ex/ROOT.ML	Wed Jun 01 10:52:17 2005 +0200
    14.2 +++ b/src/FOL/ex/ROOT.ML	Wed Jun 01 12:30:49 2005 +0200
    14.3 @@ -13,7 +13,7 @@
    14.4  time_use     "foundn.ML";
    14.5  time_use_thy "Prolog";
    14.6  
    14.7 -time_use_thy "LocaleInst";
    14.8 +time_use_thy "LocaleTest";
    14.9  
   14.10  writeln"\n** Intuitionistic examples **\n";
   14.11  time_use_thy "Intuitionistic";
    15.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Jun 01 10:52:17 2005 +0200
    15.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Jun 01 12:30:49 2005 +0200
    15.3 @@ -386,11 +386,6 @@
    15.4    OuterSyntax.command "using" "augment goal facts" K.prf_decl
    15.5      (facts >> (Toplevel.print oo (Toplevel.proof o IsarThy.using_facts)));
    15.6  
    15.7 -val instantiateP =
    15.8 -  OuterSyntax.command "instantiate" "instantiate locale" K.prf_decl
    15.9 -    (P.opt_thm_name ":" -- P.xname
   15.10 -      >> (Toplevel.print oo (Toplevel.proof o IsarThy.instantiate_locale)));
   15.11 -
   15.12  
   15.13  (* proof context *)
   15.14  
   15.15 @@ -785,9 +780,9 @@
   15.16  val _ = OuterSyntax.add_keywords
   15.17   ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
   15.18    "<=", "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes", "begin",
   15.19 -  "binder", "concl", "defines", "files", "fixes", "imports", "in", "includes",
   15.20 -  "infix", "infixl", "infixr", "is", "notes", "open", "output",
   15.21 -  "overloaded", "shows", "structure", "where", "|", "\\<equiv>",
   15.22 +  "binder", "concl", "constrains", "defines", "files", "fixes", "imports",
   15.23 +  "in", "includes", "infix", "infixl", "infixr", "is", "notes", "open",
   15.24 +  "output", "overloaded", "shows", "structure", "where", "|", "\\<equiv>",
   15.25    "\\<leftharpoondown>", "\\<rightharpoonup>",
   15.26    "\\<rightleftharpoons>", "\\<subseteq>"];
   15.27  
   15.28 @@ -813,7 +808,8 @@
   15.29    forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP,
   15.30    finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP,
   15.31    redoP, undos_proofP, undoP, killP, interpretationP, interpretP,
   15.32 -  instantiateP, (*diagnostic commands*) pretty_setmarginP,
   15.33 +  (*diagnostic commands*)
   15.34 +  pretty_setmarginP,
   15.35    print_commandsP, print_contextP, print_theoryP, print_syntaxP,
   15.36    print_theoremsP, print_localesP, print_localeP,
   15.37    print_registrationsP, print_attributesP, print_simpsetP,