--- a/src/Doc/Isar_Ref/Document_Preparation.thy Mon Mar 23 15:54:41 2015 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Mon Mar 23 15:55:41 2015 +0100
@@ -44,8 +44,7 @@
@{rail \<open>
(@@{command chapter} | @@{command section} | @@{command subsection} |
- @@{command subsubsection} | @@{command text} | @@{command txt})
- @{syntax target}? @{syntax text}
+ @@{command subsubsection} | @@{command text} | @@{command txt}) @{syntax text}
;
@@{command text_raw} @{syntax text}
\<close>}
@@ -74,7 +73,7 @@
Except for @{command "text_raw"}, the text passed to any of the above
markup commands may refer to formal entities via \emph{document
antiquotations}, see also \secref{sec:antiq}. These are interpreted in the
- present theory or proof context, or the named @{text "target"}.
+ present theory or proof context.
\medskip The proof markup commands closely resemble those for theory
specifications, but have a different formal status and produce
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Mon Mar 23 15:54:41 2015 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Mon Mar 23 15:55:41 2015 +0100
@@ -99,8 +99,7 @@
@{rail \<open>
(@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
- @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
- @{syntax target}? \<newline>
+ @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set}) \<newline>
@{syntax "fixes"} (@'for' @{syntax "fixes"})? (@'where' clauses)? \<newline>
(@'monos' @{syntax thmrefs})?
;
@@ -266,9 +265,9 @@
\end{matharray}
@{rail \<open>
- @@{command (HOL) primrec} @{syntax target}? @{syntax "fixes"} @'where' equations
+ @@{command (HOL) primrec} @{syntax "fixes"} @'where' equations
;
- (@@{command (HOL) fun} | @@{command (HOL) function}) @{syntax target}? functionopts?
+ (@@{command (HOL) fun} | @@{command (HOL) function}) functionopts?
@{syntax "fixes"} \<newline> @'where' equations
;
@@ -575,8 +574,7 @@
\end{matharray}
@{rail \<open>
- @@{command (HOL) partial_function} @{syntax target}?
- '(' @{syntax nameref} ')' @{syntax "fixes"} \<newline>
+ @@{command (HOL) partial_function} '(' @{syntax nameref} ')' @{syntax "fixes"} \<newline>
@'where' @{syntax thmdecl}? @{syntax prop}
\<close>}
@@ -1592,25 +1590,25 @@
\end{matharray}
@{rail \<open>
- @@{command (HOL) setup_lifting} \<newline>
- @{syntax thmref} @{syntax thmref}? (@'parametric' @{syntax thmref})?;
+ @@{command (HOL) setup_lifting} @{syntax thmref} @{syntax thmref}? \<newline>
+ (@'parametric' @{syntax thmref})?
\<close>}
@{rail \<open>
@@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type} @{syntax mixfix}? \<newline>
- 'is' @{syntax term} (@'parametric' (@{syntax thmref}+))?;
+ 'is' @{syntax term} (@'parametric' (@{syntax thmref}+))?
\<close>}
@{rail \<open>
- @@{command (HOL) lifting_forget} @{syntax nameref};
+ @@{command (HOL) lifting_forget} @{syntax nameref}
\<close>}
@{rail \<open>
- @@{command (HOL) lifting_update} @{syntax nameref};
+ @@{command (HOL) lifting_update} @{syntax nameref}
\<close>}
@{rail \<open>
- @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})?;
+ @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})?
\<close>}
\begin{description}
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Mon Mar 23 15:54:41 2015 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Mon Mar 23 15:55:41 2015 +0100
@@ -521,10 +521,10 @@
entities within the current context.
@{rail \<open>
- (@@{command type_notation} | @@{command no_type_notation}) @{syntax target}?
- @{syntax mode}? \<newline> (@{syntax nameref} @{syntax mixfix} + @'and')
+ (@@{command type_notation} | @@{command no_type_notation}) @{syntax mode}? \<newline>
+ (@{syntax nameref} @{syntax mixfix} + @'and')
;
- (@@{command notation} | @@{command no_notation}) @{syntax target}? @{syntax mode}? \<newline>
+ (@@{command notation} | @@{command no_notation}) @{syntax mode}? \<newline>
(@{syntax nameref} @{syntax mixfix} + @'and')
;
@@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and')
@@ -1165,6 +1165,8 @@
@{attribute_def syntax_ast_stats} & : & @{text attribute} & default @{text false} \\
\end{tabular}
+ \medskip
+
Unlike mixfix notation for existing formal entities
(\secref{sec:notation}), raw syntax declarations provide full access
to the priority grammar of the inner syntax, without any sanity
--- a/src/Doc/Isar_Ref/Proof.thy Mon Mar 23 15:54:41 2015 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy Mon Mar 23 15:55:41 2015 +0100
@@ -432,7 +432,7 @@
@{rail \<open>
(@@{command lemma} | @@{command theorem} | @@{command corollary} |
@@{command schematic_lemma} | @@{command schematic_theorem} |
- @@{command schematic_corollary}) @{syntax target}? (goal | longgoal)
+ @@{command schematic_corollary}) (goal | longgoal)
;
(@@{command have} | @@{command show} | @@{command hence} | @@{command thus}) goal
;
@@ -935,8 +935,7 @@
\end{matharray}
@{rail \<open>
- @@{command method_setup} @{syntax target}?
- @{syntax name} '=' @{syntax text} @{syntax text}?
+ @@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
\<close>}
\begin{description}
--- a/src/Doc/Isar_Ref/Spec.thy Mon Mar 23 15:54:41 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Mon Mar 23 15:55:41 2015 +0100
@@ -160,20 +160,24 @@
(global) "end"} has a different meaning: it concludes the theory
itself (\secref{sec:begin-thy}).
- \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any
- local theory command specifies an immediate target, e.g.\
- ``@{command "definition"}~@{text "(\<IN> c) \<dots>"}'' or ``@{command
- "theorem"}~@{text "(\<IN> c) \<dots>"}''. This works both in a local or
- global theory context; the current target context will be suspended
- for this command only. Note that ``@{text "(\<IN> -)"}'' will
- always produce a global result independently of the current target
- context.
+ \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any local
+ theory command specifies an immediate target, e.g.\ ``@{command
+ "definition"}~@{text "(\<IN> c)"}'' or ``@{command "theorem"}~@{text
+ "(\<IN> c)"}''. This works both in a local or global theory context; the
+ current target context will be suspended for this command only. Note that
+ ``@{text "(\<IN> -)"}'' will always produce a global result independently
+ of the current target context.
\end{description}
- The exact meaning of results produced within a local theory context
- depends on the underlying target infrastructure (locale, type class
- etc.). The general idea is as follows, considering a context named
+ Any specification element that operates on @{text local_theory} according
+ to this manual implicitly allows the above target syntax @{text
+ "("}@{keyword "in"}~@{text "c)"}, but individual syntax diagrams omit that
+ aspect for clarity.
+
+ \medskip The exact meaning of results produced within a local theory
+ context depends on the underlying target infrastructure (locale, type
+ class etc.). The general idea is as follows, considering a context named
@{text c} with parameter @{text x} and assumption @{text "A[x]"}.
Definitions are exported by introducing a global version with
@@ -188,11 +192,7 @@
generalizing the parameters of the context. For example, @{text "a:
B[x]"} becomes @{text "c.a: A[?x] \<Longrightarrow> B[?x]"}, again for arbitrary
@{text "?x"}.
-
- \medskip The Isabelle/HOL library contains numerous applications of
- locales and classes, e.g.\ see @{file "~~/src/HOL/Algebra"}. An
- example for an unnamed auxiliary contexts is given in @{file
- "~~/src/HOL/Isar_Examples/Group_Context.thy"}.\<close>
+\<close>
section \<open>Bundled declarations \label{sec:bundle}\<close>
@@ -221,8 +221,8 @@
locale interpretation (\secref{sec:locale}).
@{rail \<open>
- @@{command bundle} @{syntax target}? \<newline>
- @{syntax name} '=' @{syntax thmrefs} (@'for' (@{syntax vars} + @'and'))?
+ @@{command bundle} @{syntax name} '=' @{syntax thmrefs}
+ (@'for' (@{syntax vars} + @'and'))?
;
(@@{command include} | @@{command including}) (@{syntax nameref}+)
;
@@ -284,10 +284,9 @@
``abbreviation''.
@{rail \<open>
- @@{command definition} @{syntax target}? \<newline>
- (decl @'where')? @{syntax thmdecl}? @{syntax prop}
+ @@{command definition} (decl @'where')? @{syntax thmdecl}? @{syntax prop}
;
- @@{command abbreviation} @{syntax target}? @{syntax mode}? \<newline>
+ @@{command abbreviation} @{syntax mode}? \<newline>
(decl @'where')? @{syntax prop}
;
@@ -399,9 +398,9 @@
@{rail \<open>
(@@{command declaration} | @@{command syntax_declaration})
- ('(' @'pervasive' ')')? \<newline> @{syntax target}? @{syntax text}
+ ('(' @'pervasive' ')')? \<newline> @{syntax text}
;
- @@{command declare} @{syntax target}? (@{syntax thmrefs} + @'and')
+ @@{command declare} (@{syntax thmrefs} + @'and')
\<close>}
\begin{description}
@@ -923,7 +922,7 @@
@@{command instance} (() | (@{syntax nameref} + @'and') '::' @{syntax arity} |
@{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} )
;
- @@{command subclass} @{syntax target}? @{syntax nameref}
+ @@{command subclass} @{syntax nameref}
;
@@{command class_deps} ( ( @{syntax sort} | ( '(' ( @{syntax sort} + @'|' ) ')' ) ) \<newline>
( @{syntax sort} | ( '(' ( @{syntax sort} + @'|' ) ')' ) )? )?
@@ -1143,8 +1142,7 @@
(@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
@@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
;
- @@{command attribute_setup} @{syntax target}?
- @{syntax name} '=' @{syntax text} @{syntax text}?
+ @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
\<close>}
\begin{description}
@@ -1408,11 +1406,10 @@
\end{matharray}
@{rail \<open>
- (@@{command lemmas} | @@{command theorems}) @{syntax target}? \<newline>
- (@{syntax thmdef}? @{syntax thmrefs} + @'and')
+ (@@{command lemmas} | @@{command theorems}) (@{syntax thmdef}? @{syntax thmrefs} + @'and') \<newline>
(@'for' (@{syntax vars} + @'and'))?
;
- @@{command named_theorems} @{syntax target}?
+ @@{command named_theorems}
(@{syntax name} @{syntax text}? + @'and')
\<close>}