--- a/doc-src/IsarImplementation/Thy/Prelim.thy Mon May 02 15:13:10 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Mon May 02 17:43:42 2011 +0200
@@ -593,14 +593,14 @@
\begin{mldecls}
@{index_ML Config.get: "Proof.context -> 'a Config.T -> 'a"} \\
@{index_ML Config.map: "'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context"} \\
- @{index_ML Attrib.config_bool: "string -> (Context.generic -> bool) ->
- bool Config.T * (theory -> theory)"} \\
- @{index_ML Attrib.config_int: "string -> (Context.generic -> int) ->
- int Config.T * (theory -> theory)"} \\
- @{index_ML Attrib.config_real: "string -> (Context.generic -> real) ->
- real Config.T * (theory -> theory)"} \\
- @{index_ML Attrib.config_string: "string -> (Context.generic -> string) ->
- string Config.T * (theory -> theory)"} \\
+ @{index_ML Attrib.setup_config_bool: "binding -> (Context.generic -> bool) ->
+ bool Config.T"} \\
+ @{index_ML Attrib.setup_config_int: "binding -> (Context.generic -> int) ->
+ int Config.T"} \\
+ @{index_ML Attrib.setup_config_real: "binding -> (Context.generic -> real) ->
+ real Config.T"} \\
+ @{index_ML Attrib.setup_config_string: "binding -> (Context.generic -> string) ->
+ string Config.T"} \\
\end{mldecls}
\begin{description}
@@ -611,13 +611,13 @@
\item @{ML Config.map}~@{text "config f ctxt"} updates the context
by updating the value of @{text "config"}.
- \item @{text "(config, setup) ="}~@{ML Attrib.config_bool}~@{text
- "name default"} creates a named configuration option of type
- @{ML_type bool}, with the given @{text "default"} depending on the
- application context. The resulting @{text "config"} can be used to
- get/map its value in a given context. The @{text "setup"} function
- needs to be applied to the theory initially, in order to make
- concrete declaration syntax available to the user.
+ \item @{text "config ="}~@{ML Attrib.setup_config_bool}~@{text "name
+ default"} creates a named configuration option of type @{ML_type
+ bool}, with the given @{text "default"} depending on the application
+ context. The resulting @{text "config"} can be used to get/map its
+ value in a given context. There is an implicit update of the
+ background theory that registers the option as attribute with some
+ concrete syntax.
\item @{ML Attrib.config_int}, @{ML Attrib.config_real}, and @{ML
Attrib.config_string} work like @{ML Attrib.config_bool}, but for
@@ -631,10 +631,9 @@
default value @{ML false}. *}
ML {*
- val (my_flag, my_flag_setup) =
- Attrib.config_bool "my_flag" (K false)
+ val my_flag =
+ Attrib.setup_config_bool @{binding my_flag} (K false)
*}
-setup my_flag_setup
text {* Now the user can refer to @{attribute my_flag} in
declarations, while ML tools can retrieve the current value from the
@@ -659,10 +658,9 @@
(floating-point numbers). *}
ML {*
- val (airspeed_velocity, airspeed_velocity_setup) =
- Attrib.config_real "airspeed_velocity" (K 0.0)
+ val airspeed_velocity =
+ Attrib.setup_config_real @{binding airspeed_velocity} (K 0.0)
*}
-setup airspeed_velocity_setup
declare [[airspeed_velocity = 10]]
declare [[airspeed_velocity = 9.9]]
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Mon May 02 15:13:10 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Mon May 02 17:43:42 2011 +0200
@@ -797,14 +797,14 @@
\begin{mldecls}
\indexdef{}{ML}{Config.get}\verb|Config.get: Proof.context -> 'a Config.T -> 'a| \\
\indexdef{}{ML}{Config.map}\verb|Config.map: 'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context| \\
- \indexdef{}{ML}{Attrib.config\_bool}\verb|Attrib.config_bool: string -> (Context.generic -> bool) ->|\isasep\isanewline%
-\verb| bool Config.T * (theory -> theory)| \\
- \indexdef{}{ML}{Attrib.config\_int}\verb|Attrib.config_int: string -> (Context.generic -> int) ->|\isasep\isanewline%
-\verb| int Config.T * (theory -> theory)| \\
- \indexdef{}{ML}{Attrib.config\_real}\verb|Attrib.config_real: string -> (Context.generic -> real) ->|\isasep\isanewline%
-\verb| real Config.T * (theory -> theory)| \\
- \indexdef{}{ML}{Attrib.config\_string}\verb|Attrib.config_string: string -> (Context.generic -> string) ->|\isasep\isanewline%
-\verb| string Config.T * (theory -> theory)| \\
+ \indexdef{}{ML}{Attrib.setup\_config\_bool}\verb|Attrib.setup_config_bool: binding -> (Context.generic -> bool) ->|\isasep\isanewline%
+\verb| bool Config.T| \\
+ \indexdef{}{ML}{Attrib.setup\_config\_int}\verb|Attrib.setup_config_int: binding -> (Context.generic -> int) ->|\isasep\isanewline%
+\verb| int Config.T| \\
+ \indexdef{}{ML}{Attrib.setup\_config\_real}\verb|Attrib.setup_config_real: binding -> (Context.generic -> real) ->|\isasep\isanewline%
+\verb| real Config.T| \\
+ \indexdef{}{ML}{Attrib.setup\_config\_string}\verb|Attrib.setup_config_string: binding -> (Context.generic -> string) ->|\isasep\isanewline%
+\verb| string Config.T| \\
\end{mldecls}
\begin{description}
@@ -815,12 +815,11 @@
\item \verb|Config.map|~\isa{config\ f\ ctxt} updates the context
by updating the value of \isa{config}.
- \item \isa{{\isaliteral{28}{\isacharparenleft}}config{\isaliteral{2C}{\isacharcomma}}\ setup{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}}~\verb|Attrib.config_bool|~\isa{name\ default} creates a named configuration option of type
- \verb|bool|, with the given \isa{default} depending on the
- application context. The resulting \isa{config} can be used to
- get/map its value in a given context. The \isa{setup} function
- needs to be applied to the theory initially, in order to make
- concrete declaration syntax available to the user.
+ \item \isa{config\ {\isaliteral{3D}{\isacharequal}}}~\verb|Attrib.setup_config_bool|~\isa{name\ default} creates a named configuration option of type \verb|bool|, with the given \isa{default} depending on the application
+ context. The resulting \isa{config} can be used to get/map its
+ value in a given context. There is an implicit update of the
+ background theory that registers the option as attribute with some
+ concrete syntax.
\item \verb|Attrib.config_int|, \verb|Attrib.config_real|, and \verb|Attrib.config_string| work like \verb|Attrib.config_bool|, but for
types \verb|int| and \verb|string|, respectively.
@@ -863,11 +862,13 @@
\isatagML
\isacommand{ML}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
-\ \ val\ {\isaliteral{28}{\isacharparenleft}}my{\isaliteral{5F}{\isacharunderscore}}flag{\isaliteral{2C}{\isacharcomma}}\ my{\isaliteral{5F}{\isacharunderscore}}flag{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}config{\isaliteral{5F}{\isacharunderscore}}bool\ {\isaliteral{22}{\isachardoublequote}}my{\isaliteral{5F}{\isacharunderscore}}flag{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}K\ false{\isaliteral{29}{\isacharparenright}}\isanewline
-{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
-\isacommand{setup}\isamarkupfalse%
-\ my{\isaliteral{5F}{\isacharunderscore}}flag{\isaliteral{5F}{\isacharunderscore}}setup%
+\ \ val\ my{\isaliteral{5F}{\isacharunderscore}}flag\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}setup{\isaliteral{5F}{\isacharunderscore}}config{\isaliteral{5F}{\isacharunderscore}}bool\ %
+\isaantiq
+binding\ my{\isaliteral{5F}{\isacharunderscore}}flag{}%
+\endisaantiq
+\ {\isaliteral{28}{\isacharparenleft}}K\ false{\isaliteral{29}{\isacharparenright}}\isanewline
+{\isaliteral{2A7D}{\isacharverbatimclose}}%
\endisatagML
{\isafoldML}%
%
@@ -1028,11 +1029,13 @@
\isatagML
\isacommand{ML}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
-\ \ val\ {\isaliteral{28}{\isacharparenleft}}airspeed{\isaliteral{5F}{\isacharunderscore}}velocity{\isaliteral{2C}{\isacharcomma}}\ airspeed{\isaliteral{5F}{\isacharunderscore}}velocity{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}config{\isaliteral{5F}{\isacharunderscore}}real\ {\isaliteral{22}{\isachardoublequote}}airspeed{\isaliteral{5F}{\isacharunderscore}}velocity{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}K\ {\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
-\isacommand{setup}\isamarkupfalse%
-\ airspeed{\isaliteral{5F}{\isacharunderscore}}velocity{\isaliteral{5F}{\isacharunderscore}}setup%
+\ \ val\ airspeed{\isaliteral{5F}{\isacharunderscore}}velocity\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}setup{\isaliteral{5F}{\isacharunderscore}}config{\isaliteral{5F}{\isacharunderscore}}real\ %
+\isaantiq
+binding\ airspeed{\isaliteral{5F}{\isacharunderscore}}velocity{}%
+\endisaantiq
+\ {\isaliteral{28}{\isacharparenleft}}K\ {\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
+{\isaliteral{2A7D}{\isacharverbatimclose}}%
\endisatagML
{\isafoldML}%
%
--- a/doc-src/IsarImplementation/implementation.tex Mon May 02 15:13:10 2011 +0200
+++ b/doc-src/IsarImplementation/implementation.tex Mon May 02 17:43:42 2011 +0200
@@ -23,11 +23,6 @@
\makeindex
-\railterm{lbrace,rbrace,atsign}
-\railalias{lbracesym}{\isasymlbrace}\railterm{lbracesym}
-\railalias{rbracesym}{\isasymrbrace}\railterm{rbracesym}
-\railalias{dots}{\isasymdots}\railterm{dots}
-
\begin{document}
--- a/doc-src/IsarRef/Makefile Mon May 02 15:13:10 2011 +0200
+++ b/doc-src/IsarRef/Makefile Mon May 02 17:43:42 2011 +0200
@@ -30,7 +30,6 @@
$(NAME).dvi: $(FILES) isabelle_isar.eps syms.tex
$(LATEX) $(NAME)
- $(RAIL) $(NAME)
$(BIBTEX) $(NAME)
$(LATEX) $(NAME)
$(LATEX) $(NAME)
@@ -41,7 +40,6 @@
$(NAME).pdf: $(FILES) isabelle_isar.pdf syms.tex
$(PDFLATEX) $(NAME)
- $(RAIL) $(NAME)
$(BIBTEX) $(NAME)
$(PDFLATEX) $(NAME)
$(PDFLATEX) $(NAME)
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy Mon May 02 15:13:10 2011 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Mon May 02 17:43:42 2011 +0200
@@ -185,7 +185,7 @@
@{syntax_def antiquotation}:
@@{antiquotation theory} options @{syntax name} |
@@{antiquotation thm} options styles @{syntax thmrefs} |
- @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} |
+ @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
@@{antiquotation prop} options styles @{syntax prop} |
@@{antiquotation term} options styles @{syntax term} |
@@{antiquotation term_type} options styles @{syntax term} |
@@ -212,7 +212,7 @@
styles: '(' (style + ',') ')'
;
style: (@{syntax name} +)
- "} %% FIXME check lemma
+ "}
Note that the syntax of antiquotations may \emph{not} include source
comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim
--- a/doc-src/IsarRef/Thy/Generic.thy Mon May 02 15:13:10 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Mon May 02 17:43:42 2011 +0200
@@ -284,7 +284,7 @@
@{rail "
(@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
@@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goalspec}?
- ( insts @{syntax thmref} | @{syntax thmrefs} )
+ ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
;
@@{method subgoal_tac} @{syntax goalspec}? (@{syntax prop} +)
;
@@ -295,8 +295,8 @@
(@@{method tactic} | @@{method raw_tactic}) @{syntax text}
;
- insts: ((@{syntax name} '=' @{syntax term}) + @'and') @'in'
- "} % FIXME check use of insts
+ dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and')
+ "}
\begin{description}
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon May 02 15:13:10 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon May 02 17:43:42 2011 +0200
@@ -389,19 +389,19 @@
\end{matharray}
@{rail "
- @@{command (HOL) enriched_type} (prefix ':')? @{syntax term}
+ @@{command (HOL) enriched_type} (@{syntax name} ':')? @{syntax term}
;
- "} % FIXME check prefix
+ "}
\begin{description}
- \item @{command (HOL) "enriched_type"} allows to prove and register
- properties about the functorial structure of type constructors;
- these properties then can be used by other packages to
- deal with those type constructors in certain type constructions.
- Characteristic theorems are noted in the current local theory; by
- default, they are prefixed with the base name of the type constructor,
- an explicit prefix can be given alternatively.
+ \item @{command (HOL) "enriched_type"}~@{text "prefix: m"} allows to
+ prove and register properties about the functorial structure of type
+ constructors. These properties then can be used by other packages
+ to deal with those type constructors in certain type constructions.
+ Characteristic theorems are noted in the current local theory. By
+ default, they are prefixed with the base name of the type
+ constructor, an explicit prefix can be given alternatively.
The given term @{text "m"} is considered as \emph{mapper} for the
corresponding type constructor and must conform to the following
@@ -588,17 +588,18 @@
@{rail "
@@{command (HOL) partial_function} @{syntax target}?
- '(' mode ')' @{syntax \"fixes\"} \\ @'where' @{syntax thmdecl}? @{syntax prop}
- "} % FIXME check mode
+ '(' @{syntax nameref} ')' @{syntax \"fixes\"} \\
+ @'where' @{syntax thmdecl}? @{syntax prop}
+ "}
\begin{description}
- \item @{command (HOL) "partial_function"} defines recursive
- functions based on fixpoints in complete partial orders. No
- termination proof is required from the user or constructed
- internally. Instead, the possibility of non-termination is modelled
- explicitly in the result type, which contains an explicit bottom
- element.
+ \item @{command (HOL) "partial_function"}~@{text "(mode)"} defines
+ recursive functions based on fixpoints in complete partial
+ orders. No termination proof is required from the user or
+ constructed internally. Instead, the possibility of non-termination
+ is modelled explicitly in the result type, which contains an
+ explicit bottom element.
Pattern matching and mutual recursion are currently not supported.
Thus, the specification consists of a single function described by a
--- a/doc-src/IsarRef/Thy/Proof.thy Mon May 02 15:13:10 2011 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy Mon May 02 17:43:42 2011 +0200
@@ -444,7 +444,7 @@
goal: (@{syntax props} + @'and')
;
- longgoal: @{syntax thmdecl}? (@{syntax contextelem} * ) conclusion
+ longgoal: @{syntax thmdecl}? (@{syntax context_elem} * ) conclusion
;
conclusion: @'shows' goal | @'obtains' (@{syntax parname}? case + '|')
;
@@ -458,7 +458,7 @@
\<phi>"} to be put back into the target context. An additional @{syntax
context} specification may build up an initial proof context for the
subsequent claim; this includes local definitions and syntax as
- well, see the definition of @{syntax contextelem} in
+ well, see the definition of @{syntax context_elem} in
\secref{sec:locale}.
\item @{command "theorem"}~@{text "a: \<phi>"} and @{command
@@ -1278,7 +1278,7 @@
;
@@{method induct} ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
;
- @@{method coinduct} insts taking rule?
+ @@{method coinduct} @{syntax insts} taking rule?
;
rule: ('type' | 'pred' | 'set') ':' (@{syntax nameref} +) | 'rule' ':' (@{syntax thmref} +)
@@ -1289,7 +1289,7 @@
;
arbitrary: 'arbitrary' ':' ((@{syntax term} * ) @'and' +)
;
- taking: 'taking' ':' insts
+ taking: 'taking' ':' @{syntax insts}
"}
\begin{description}
--- a/doc-src/IsarRef/Thy/Spec.thy Mon May 02 15:13:10 2011 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Mon May 02 17:43:42 2011 +0200
@@ -311,15 +311,15 @@
duplicate declarations.
@{rail "
- @{syntax_def localeexpr}: (instance + '+') (@'for' (@{syntax \"fixes\"} + @'and'))?
+ @{syntax_def locale_expr}: (instance + '+') (@'for' (@{syntax \"fixes\"} + @'and'))?
;
- instance: (qualifier ':')? @{syntax nameref} (posinsts | namedinsts)
+ instance: (qualifier ':')? @{syntax nameref} (pos_insts | named_insts)
;
qualifier: @{syntax name} ('?' | '!')?
;
- posinsts: ('_' | @{syntax term})*
+ pos_insts: ('_' | @{syntax term})*
;
- namedinsts: @'where' (@{syntax name} '=' @{syntax term} + @'and')
+ named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and')
"}
A locale instance consists of a reference to a locale and either
@@ -364,10 +364,10 @@
;
@@{command print_locale} '!'? @{syntax nameref}
;
- @{syntax_def locale}: @{syntax contextelem}+ |
- @{syntax localeexpr} ('+' (@{syntax contextelem}+))?
+ @{syntax_def locale}: @{syntax context_elem}+ |
+ @{syntax locale_expr} ('+' (@{syntax context_elem}+))?
;
- @{syntax_def contextelem}:
+ @{syntax_def context_elem}:
@'fixes' (@{syntax \"fixes\"} + @'and') |
@'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
@'assumes' (@{syntax props} + @'and') |
@@ -499,13 +499,13 @@
\end{matharray}
@{rail "
- @@{command interpretation} @{syntax localeexpr} equations?
+ @@{command interpretation} @{syntax locale_expr} equations?
;
- @@{command interpret} @{syntax localeexpr} equations?
+ @@{command interpret} @{syntax locale_expr} equations?
;
- @@{command sublocale} @{syntax nameref} ('<' | '\<subseteq>') @{syntax localeexpr} equations?
+ @@{command sublocale} @{syntax nameref} ('<' | '\<subseteq>') @{syntax locale_expr} equations?
;
- @@{command print_dependencies} '!'? @{syntax localeexpr}
+ @@{command print_dependencies} '!'? @{syntax locale_expr}
;
@@{command print_interps} @{syntax nameref}
;
@@ -640,8 +640,8 @@
@{rail "
@@{command class} @{syntax name} '='
- ((superclassexpr '+' (@{syntax contextelem}+)) |
- superclassexpr | (@{syntax contextelem}+)) \\
+ ((@{syntax nameref} '+' (@{syntax context_elem}+)) |
+ @{syntax nameref} | (@{syntax context_elem}+)) \\
@'begin'?
;
@@{command instantiation} (@{syntax nameref} + @'and') '::' @{syntax arity} @'begin'
@@ -658,9 +658,7 @@
;
@@{command class_deps}
;
-
- superclassexpr: @{syntax nameref} | (@{syntax nameref} '+' superclassexpr)
- "} %% FIXME check superclassexpr
+ "}
\begin{description}
@@ -821,9 +819,9 @@
@{rail "
@@{command overloading} \\
- ( @{syntax string} ( '==' | '\<equiv>' ) @{syntax term}
+ ( @{syntax name} ( '==' | '\<equiv>' ) @{syntax term}
( '(' @'unchecked' ')' )? +) @'begin'
- "} %% FIXME check string vs. name
+ "}
\begin{description}
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Mon May 02 15:13:10 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Mon May 02 17:43:42 2011 +0200
@@ -235,7 +235,7 @@
\rail@nont{\isa{antiquotation}}[]
\rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
\rail@end
-\rail@begin{21}{\indexdef{}{syntax}{antiquotation}\hypertarget{syntax.antiquotation}{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}}
+\rail@begin{22}{\indexdef{}{syntax}{antiquotation}\hypertarget{syntax.antiquotation}{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}}
\rail@bar
\rail@term{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}}[]
\rail@nont{\isa{options}}[]
@@ -251,77 +251,81 @@
\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
\rail@term{\isa{\isakeyword{by}}}[]
\rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[]
+\rail@bar
\rail@nextbar{3}
+\rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[]
+\rail@endbar
+\rail@nextbar{4}
\rail@term{\hyperlink{antiquotation.prop}{\mbox{\isa{prop}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\isa{styles}}[]
\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
-\rail@nextbar{4}
+\rail@nextbar{5}
\rail@term{\hyperlink{antiquotation.term}{\mbox{\isa{term}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\isa{styles}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@nextbar{5}
+\rail@nextbar{6}
\rail@term{\hyperlink{antiquotation.term-type}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}type}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\isa{styles}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@nextbar{6}
-\rail@term{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}}[]
-\rail@nont{\isa{options}}[]
-\rail@nont{\isa{styles}}[]
-\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@nextbar{7}
+\rail@term{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}}[]
+\rail@nont{\isa{options}}[]
+\rail@nont{\isa{styles}}[]
+\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
+\rail@nextbar{8}
\rail@term{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@nextbar{8}
+\rail@nextbar{9}
\rail@term{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@nextbar{9}
+\rail@nextbar{10}
\rail@term{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
-\rail@nextbar{10}
+\rail@nextbar{11}
\rail@term{\hyperlink{antiquotation.type}{\mbox{\isa{type}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{11}
+\rail@nextbar{12}
\rail@term{\hyperlink{antiquotation.class}{\mbox{\isa{class}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{12}
-\rail@term{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}}[]
-\rail@nont{\isa{options}}[]
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@nextbar{13}
+\rail@term{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}}[]
+\rail@nont{\isa{options}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@nextbar{14}
\rail@term{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}}[]
\rail@nont{\isa{options}}[]
-\rail@nextbar{14}
+\rail@nextbar{15}
\rail@term{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}}[]
\rail@nont{\isa{options}}[]
-\rail@nextbar{15}
+\rail@nextbar{16}
\rail@term{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@nextbar{16}
+\rail@nextbar{17}
\rail@term{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isaliteral{5F}{\isacharunderscore}}prf}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@nextbar{17}
+\rail@nextbar{18}
\rail@term{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{18}
+\rail@nextbar{19}
\rail@term{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}type}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{19}
+\rail@nextbar{20}
\rail@term{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}struct}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextbar{20}
+\rail@nextbar{21}
\rail@term{\hyperlink{antiquotation.file}{\mbox{\isa{file}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
@@ -364,7 +368,7 @@
\rail@endplus
\rail@end
\end{railoutput}
- %% FIXME check lemma
+
Note that the syntax of antiquotations may \emph{not} include source
comments \verb|(*|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}~\verb|*)| nor verbatim
--- a/doc-src/IsarRef/Thy/document/Generic.tex Mon May 02 15:13:10 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Mon May 02 17:43:42 2011 +0200
@@ -419,7 +419,8 @@
\rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
\rail@endbar
\rail@bar
-\rail@nont{\isa{insts}}[]
+\rail@nont{\isa{dynamic{\isaliteral{5F}{\isacharunderscore}}insts}}[]
+\rail@term{\isa{\isakeyword{in}}}[]
\rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
\rail@nextbar{1}
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
@@ -466,7 +467,7 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
\rail@end
-\rail@begin{2}{\isa{insts}}
+\rail@begin{2}{\isa{dynamic{\isaliteral{5F}{\isacharunderscore}}insts}}
\rail@plus
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
@@ -474,10 +475,9 @@
\rail@nextplus{1}
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
-\rail@term{\isa{\isakeyword{in}}}[]
\rail@end
\end{railoutput}
- % FIXME check use of insts
+
\begin{description}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon May 02 15:13:10 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon May 02 17:43:42 2011 +0200
@@ -503,23 +503,23 @@
\rail@term{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
\rail@bar
\rail@nextbar{1}
-\rail@nont{\isa{prefix}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
\rail@endbar
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@end
\end{railoutput}
- % FIXME check prefix
+
\begin{description}
- \item \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}} allows to prove and register
- properties about the functorial structure of type constructors;
- these properties then can be used by other packages to
- deal with those type constructors in certain type constructions.
- Characteristic theorems are noted in the current local theory; by
- default, they are prefixed with the base name of the type constructor,
- an explicit prefix can be given alternatively.
+ \item \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}prefix{\isaliteral{3A}{\isacharcolon}}\ m{\isaliteral{22}{\isachardoublequote}}} allows to
+ prove and register properties about the functorial structure of type
+ constructors. These properties then can be used by other packages
+ to deal with those type constructors in certain type constructions.
+ Characteristic theorems are noted in the current local theory. By
+ default, they are prefixed with the base name of the type
+ constructor, an explicit prefix can be given alternatively.
The given term \isa{{\isaliteral{22}{\isachardoublequote}}m{\isaliteral{22}{\isachardoublequote}}} is considered as \emph{mapper} for the
corresponding type constructor and must conform to the following
@@ -788,7 +788,7 @@
\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
\rail@endbar
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
-\rail@nont{\isa{mode}}[]
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
\rail@cr{3}
@@ -800,16 +800,16 @@
\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
\rail@end
\end{railoutput}
- % FIXME check mode
+
\begin{description}
- \item \hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}} defines recursive
- functions based on fixpoints in complete partial orders. No
- termination proof is required from the user or constructed
- internally. Instead, the possibility of non-termination is modelled
- explicitly in the result type, which contains an explicit bottom
- element.
+ \item \hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mode{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} defines
+ recursive functions based on fixpoints in complete partial
+ orders. No termination proof is required from the user or
+ constructed internally. Instead, the possibility of non-termination
+ is modelled explicitly in the result type, which contains an
+ explicit bottom element.
Pattern matching and mutual recursion are currently not supported.
Thus, the specification consists of a single function described by a
--- a/doc-src/IsarRef/Thy/document/Proof.tex Mon May 02 15:13:10 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Mon May 02 17:43:42 2011 +0200
@@ -596,7 +596,7 @@
\rail@endbar
\rail@plus
\rail@nextplus{1}
-\rail@cnont{\hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}}}[]
+\rail@cnont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
\rail@endplus
\rail@nont{\isa{conclusion}}[]
\rail@end
@@ -638,7 +638,7 @@
\item \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} enters proof mode with
\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} as main goal, eventually resulting in some fact \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} to be put back into the target context. An additional \hyperlink{syntax.context}{\mbox{\isa{context}}} specification may build up an initial proof context for the
subsequent claim; this includes local definitions and syntax as
- well, see the definition of \hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}} in
+ well, see the definition of \hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}} in
\secref{sec:locale}.
\item \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} and \hyperlink{command.corollary}{\mbox{\isa{\isacommand{corollary}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} are essentially the same as \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}}, but the facts are internally marked as
@@ -1753,7 +1753,7 @@
\rail@end
\rail@begin{2}{\isa{}}
\rail@term{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}}[]
-\rail@nont{\isa{insts}}[]
+\rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
\rail@nont{\isa{taking}}[]
\rail@bar
\rail@nextbar{1}
@@ -1821,7 +1821,7 @@
\rail@begin{1}{\isa{taking}}
\rail@term{\isa{taking}}[]
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
-\rail@nont{\isa{insts}}[]
+\rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
\rail@end
\end{railoutput}
--- a/doc-src/IsarRef/Thy/document/Spec.tex Mon May 02 15:13:10 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon May 02 17:43:42 2011 +0200
@@ -470,7 +470,7 @@
duplicate declarations.
\begin{railoutput}
-\rail@begin{3}{\indexdef{}{syntax}{localeexpr}\hypertarget{syntax.localeexpr}{\hyperlink{syntax.localeexpr}{\mbox{\isa{localeexpr}}}}}
+\rail@begin{3}{\indexdef{}{syntax}{locale\_expr}\hypertarget{syntax.locale-expr}{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}}
\rail@plus
\rail@nont{\isa{instance}}[]
\rail@nextplus{1}
@@ -494,9 +494,9 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
\rail@bar
-\rail@nont{\isa{posinsts}}[]
+\rail@nont{\isa{pos{\isaliteral{5F}{\isacharunderscore}}insts}}[]
\rail@nextbar{1}
-\rail@nont{\isa{namedinsts}}[]
+\rail@nont{\isa{named{\isaliteral{5F}{\isacharunderscore}}insts}}[]
\rail@endbar
\rail@end
\rail@begin{3}{\isa{qualifier}}
@@ -510,7 +510,7 @@
\rail@endbar
\rail@endbar
\rail@end
-\rail@begin{3}{\isa{posinsts}}
+\rail@begin{3}{\isa{pos{\isaliteral{5F}{\isacharunderscore}}insts}}
\rail@plus
\rail@nextplus{1}
\rail@bar
@@ -520,7 +520,7 @@
\rail@endbar
\rail@endplus
\rail@end
-\rail@begin{2}{\isa{namedinsts}}
+\rail@begin{2}{\isa{named{\isaliteral{5F}{\isacharunderscore}}insts}}
\rail@term{\isa{\isakeyword{where}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
@@ -596,22 +596,22 @@
\rail@begin{5}{\indexdef{}{syntax}{locale}\hypertarget{syntax.locale}{\hyperlink{syntax.locale}{\mbox{\isa{locale}}}}}
\rail@bar
\rail@plus
-\rail@nont{\hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}}}[]
+\rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
\rail@nextplus{1}
\rail@endplus
\rail@nextbar{2}
-\rail@nont{\hyperlink{syntax.localeexpr}{\mbox{\isa{localeexpr}}}}[]
+\rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
\rail@bar
\rail@nextbar{3}
\rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
\rail@plus
-\rail@nont{\hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}}}[]
+\rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
\rail@nextplus{4}
\rail@endplus
\rail@endbar
\rail@endbar
\rail@end
-\rail@begin{12}{\indexdef{}{syntax}{contextelem}\hypertarget{syntax.contextelem}{\hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}}}}
+\rail@begin{12}{\indexdef{}{syntax}{context\_elem}\hypertarget{syntax.context-elem}{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}}
\rail@bar
\rail@term{\isa{\isakeyword{fixes}}}[]
\rail@plus
@@ -789,7 +789,7 @@
\begin{railoutput}
\rail@begin{2}{\isa{}}
\rail@term{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}}[]
-\rail@nont{\hyperlink{syntax.localeexpr}{\mbox{\isa{localeexpr}}}}[]
+\rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\isa{equations}}[]
@@ -797,7 +797,7 @@
\rail@end
\rail@begin{2}{\isa{}}
\rail@term{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}}[]
-\rail@nont{\hyperlink{syntax.localeexpr}{\mbox{\isa{localeexpr}}}}[]
+\rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\isa{equations}}[]
@@ -811,7 +811,7 @@
\rail@nextbar{1}
\rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]
\rail@endbar
-\rail@nont{\hyperlink{syntax.localeexpr}{\mbox{\isa{localeexpr}}}}[]
+\rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\isa{equations}}[]
@@ -823,7 +823,7 @@
\rail@nextbar{1}
\rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
\rail@endbar
-\rail@nont{\hyperlink{syntax.localeexpr}{\mbox{\isa{localeexpr}}}}[]
+\rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
\rail@end
\rail@begin{1}{\isa{}}
\rail@term{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}}[]
@@ -974,17 +974,17 @@
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
\rail@bar
-\rail@nont{\isa{superclassexpr}}[]
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
\rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
\rail@plus
-\rail@nont{\hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}}}[]
+\rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
\rail@nextplus{1}
\rail@endplus
\rail@nextbar{2}
-\rail@nont{\isa{superclassexpr}}[]
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
\rail@nextbar{3}
\rail@plus
-\rail@nont{\hyperlink{syntax.contextelem}{\mbox{\isa{contextelem}}}}[]
+\rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
\rail@nextplus{4}
\rail@endplus
\rail@endbar
@@ -1042,17 +1042,8 @@
\rail@begin{1}{\isa{}}
\rail@term{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
\rail@end
-\rail@begin{2}{\isa{superclassexpr}}
-\rail@bar
-\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
-\rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
-\rail@nont{\isa{superclassexpr}}[]
-\rail@endbar
-\rail@end
\end{railoutput}
- %% FIXME check superclassexpr
+
\begin{description}
@@ -1214,7 +1205,7 @@
\rail@term{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}}[]
\rail@cr{2}
\rail@plus
-\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@bar
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}}}[]
\rail@nextbar{3}
@@ -1232,7 +1223,7 @@
\rail@term{\isa{\isakeyword{begin}}}[]
\rail@end
\end{railoutput}
- %% FIXME check string vs. name
+
\begin{description}
--- a/doc-src/IsarRef/isar-ref.tex Mon May 02 15:13:10 2011 +0200
+++ b/doc-src/IsarRef/isar-ref.tex Mon May 02 17:43:42 2011 +0200
@@ -36,39 +36,6 @@
\makeindex
-\railterm{percent,ppercent,underscore,lbrace,rbrace,atsign}
-\railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
-\railterm{name,nameref,text,type,term,prop,atom}
-
-\railalias{ident}{\railtok{ident}}
-\railalias{longident}{\railtok{longident}}
-\railalias{symident}{\railtok{symident}}
-\railalias{var}{\railtok{var}}
-\railalias{textvar}{\railtok{textvar}}
-\railalias{typefree}{\railtok{typefree}}
-\railalias{typevar}{\railtok{typevar}}
-\railalias{nat}{\railtok{nat}}
-\railalias{string}{\railtok{string}}
-\railalias{verbatim}{\railtok{verbatim}}
-\railalias{keyword}{\railtok{keyword}}
-
-\railalias{name}{\railqtok{name}}
-\railalias{nameref}{\railqtok{nameref}}
-\railalias{text}{\railqtok{text}}
-\railalias{type}{\railqtok{type}}
-\railalias{term}{\railqtok{term}}
-\railalias{prop}{\railqtok{prop}}
-\railalias{atom}{\railqtok{atom}}
-
-\railalias{subseteq}{\isasymsubseteq}\railterm{subseteq}
-\railalias{equiv}{\isasymequiv}\railterm{equiv}
-\railalias{rightleftharpoons}{\isasymrightleftharpoons}\railterm{rightleftharpoons}
-\railalias{rightharpoonup}{\isasymrightharpoonup}\railterm{rightharpoonup}
-\railalias{leftharpoondown}{\isasymleftharpoondown}\railterm{leftharpoondown}
-\railalias{verblbrace}{\texttt{\ttlbrace*}}\railterm{verblbrace}
-\railalias{verbrbrace}{\texttt{*\ttrbrace}}\railterm{verbrbrace}
-
-
\chardef\charbackquote=`\`
\newcommand{\backquote}{\mbox{\tt\charbackquote}}
--- a/doc-src/ZF/Makefile Mon May 02 15:13:10 2011 +0200
+++ b/doc-src/ZF/Makefile Mon May 02 17:43:42 2011 +0200
@@ -13,12 +13,9 @@
NAME = logics-ZF
FILES = logics-ZF.tex ../Logics/syntax.tex FOL.tex ZF.tex logics.sty \
- ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty \
+ ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty \
../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty ../pdfsetup.sty ../manual.bib
-rail:
- $(RAIL) $(NAME)
-
dvi: $(NAME).dvi
$(NAME).dvi: $(FILES) isabelle_zf.eps
--- a/doc-src/ZF/ZF.tex Mon May 02 15:13:10 2011 +0200
+++ b/doc-src/ZF/ZF.tex Mon May 02 17:43:42 2011 +0200
@@ -1761,27 +1761,11 @@
\subsection{Defining datatypes}
-The theory syntax for datatype definitions is shown in
-Fig.~\ref{datatype-grammar}. In order to be well-formed, a datatype
-definition has to obey the rules stated in the previous section. As a result
-the theory is extended with the new types, the constructors, and the theorems
-listed in the previous section. The quotation marks are necessary because
-they enclose general Isabelle formul\ae.
-
-\begin{figure}
-\begin{rail}
-datatype : ( 'datatype' | 'codatatype' ) datadecls;
-
-datadecls: ( '"' id arglist '"' '=' (constructor + '|') ) + 'and'
- ;
-constructor : name ( () | consargs ) ( () | ( '(' mixfix ')' ) )
- ;
-consargs : '(' ('"' var ' : ' term '"' + ',') ')'
- ;
-\end{rail}
-\caption{Syntax of datatype declarations}
-\label{datatype-grammar}
-\end{figure}
+The theory syntax for datatype definitions is shown in the
+Isabelle/Isar reference manual. In order to be well-formed, a
+datatype definition has to obey the rules stated in the previous
+section. As a result the theory is extended with the new types, the
+constructors, and the theorems listed in the previous section.
Codatatypes are declared like datatypes and are identical to them in every
respect except that they have a coinduction rule instead of an induction rule.
--- a/doc-src/ZF/logics-ZF.rai Mon May 02 15:13:10 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-\rail@i{1}{ datatype : ( 'datatype' | 'codatatype' ) datadecls; \par
-datadecls: ( '"' id arglist '"' '=' (constructor + '|') ) + 'and' ; constructor : name ( () | consargs ) ( () | ( '(' mixfix ')' ) ) ; consargs : '(' ('"' var ' : ' term '"' + ',') ')' ; }
--- a/doc-src/ZF/logics-ZF.rao Mon May 02 15:13:10 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,55 +0,0 @@
-% This file was generated by 'rail' from 'logics-ZF.rai'
-\rail@i {1}{ datatype : ( 'datatype' | 'codatatype' ) datadecls; \par
-datadecls: ( '"' id arglist '"' '=' (constructor + '|') ) + 'and' ; constructor : name ( () | consargs ) ( () | ( '(' mixfix ')' ) ) ; consargs : '(' ('"' var ' : ' term '"' + ',') ')' ; }
-\rail@o {1}{
-\rail@begin{2}{datatype}
-\rail@bar
-\rail@term{datatype}[]
-\rail@nextbar{1}
-\rail@term{codatatype}[]
-\rail@endbar
-\rail@nont{datadecls}[]
-\rail@end
-\rail@begin{3}{datadecls}
-\rail@plus
-\rail@term{"}[]
-\rail@nont{id}[]
-\rail@nont{arglist}[]
-\rail@term{"}[]
-\rail@term{=}[]
-\rail@plus
-\rail@nont{constructor}[]
-\rail@nextplus{1}
-\rail@cterm{|}[]
-\rail@endplus
-\rail@nextplus{2}
-\rail@cterm{and}[]
-\rail@endplus
-\rail@end
-\rail@begin{2}{constructor}
-\rail@nont{name}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{consargs}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@term{(}[]
-\rail@nont{mixfix}[]
-\rail@term{)}[]
-\rail@endbar
-\rail@end
-\rail@begin{2}{consargs}
-\rail@term{(}[]
-\rail@plus
-\rail@term{"}[]
-\rail@nont{var}[]
-\rail@term{ : }[]
-\rail@nont{term}[]
-\rail@term{"}[]
-\rail@nextplus{1}
-\rail@cterm{,}[]
-\rail@endplus
-\rail@term{)}[]
-\rail@end
-}
--- a/doc-src/ZF/logics-ZF.tex Mon May 02 15:13:10 2011 +0200
+++ b/doc-src/ZF/logics-ZF.tex Mon May 02 17:43:42 2011 +0200
@@ -1,7 +1,7 @@
%% $Id$
\documentclass[11pt,a4paper]{report}
\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
-\usepackage{graphicx,logics,../ttbox,../proof,../rail,latexsym}
+\usepackage{graphicx,logics,../ttbox,../proof,latexsym}
\usepackage{../pdfsetup}
%last package!
--- a/doc-src/railsetup.sty Mon May 02 15:13:10 2011 +0200
+++ b/doc-src/railsetup.sty Mon May 02 17:43:42 2011 +0200
@@ -21,22 +21,9 @@
{\begin{list}{}{\rail@param}\def\rail@expand{\relax}\makeatletter}{\end{list}}
-%% old-style content markup
-
-\railalias{percent}{\%}
-\railalias{ppercent}{\%\%}
-\railalias{underscore}{\_}
-\railalias{lbrace}{\texttt{\ttlbrace}}
-\railalias{rbrace}{\texttt{\ttrbrace}}
-\railalias{atsign}{{\at}}
+%% content markup
\def\rail@termfont{\small\ttfamily\upshape\isabellestyle{tt}}
-\def\rail@tokenfont{\small\ttfamily\upshape}
-\def\rail@nontfont{\small\rmfamily\upshape\isabellestyle{it}}
-\def\rail@annofont{\small\rmfamily\itshape}
+\def\rail@nontfont{\small\rmfamily\itshape\isabellestyle{it}}
\def\rail@namefont{\small\rmfamily\itshape\isabellestyle{it}}
-\def\rail@indexfont{\small\rmfamily\itshape}
-\newcommand{\railtterm}[1]{{\texttt{#1}}}
-\newcommand{\railtok}[1]{{\textrm{#1}}}
-\newcommand{\railqtok}[1]{{\rmfamily\textsl{#1}}}
-\newcommand{\railnonterm}[1]{{\emph{#1}}}
+
--- a/src/FOLP/IFOLP.thy Mon May 02 15:13:10 2011 +0200
+++ b/src/FOLP/IFOLP.thy Mon May 02 17:43:42 2011 +0200
@@ -69,8 +69,7 @@
*}
(*show_proofs = true displays the proof terms -- they are ENORMOUS*)
-ML {* val (show_proofs, setup_show_proofs) = Attrib.config_bool "show_proofs" (K false) *}
-setup setup_show_proofs
+ML {* val show_proofs = Attrib.setup_config_bool @{binding show_proofs} (K false) *}
print_translation (advanced) {*
let
--- a/src/HOL/Library/Sum_of_Squares.thy Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Library/Sum_of_Squares.thy Mon May 02 17:43:42 2011 +0200
@@ -38,7 +38,6 @@
the proof without calling an external prover.
*}
-setup Sum_of_Squares.setup
setup SOS_Wrapper.setup
text {* Tests *}
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Mon May 02 17:43:42 2011 +0200
@@ -24,7 +24,7 @@
(*** calling provers ***)
-val (dest_dir, setup_dest_dir) = Attrib.config_string "sos_dest_dir" (K "")
+val dest_dir = Attrib.setup_config_string @{binding sos_dest_dir} (K "")
fun filename dir name =
let
@@ -117,7 +117,7 @@
| prover "csdp" = csdp
| prover name = error ("Unknown prover: " ^ name)
-val (prover_name, setup_prover_name) = Attrib.config_string "sos_prover_name" (K "remote_csdp")
+val prover_name = Attrib.setup_config_string @{binding sos_prover_name} (K "remote_csdp")
fun call_solver ctxt opt_name =
let
@@ -140,8 +140,6 @@
fun sos_solver print method = SIMPLE_METHOD' o Sum_of_Squares.sos_tac print method
val setup =
- setup_dest_dir #>
- setup_prover_name #>
Method.setup @{binding sos}
(Scan.lift (Scan.option Parse.xname)
>> (fn opt_name => fn ctxt =>
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Mon May 02 17:43:42 2011 +0200
@@ -10,7 +10,6 @@
datatype proof_method = Certificate of RealArith.pss_tree | Prover of string -> string
val sos_tac: (RealArith.pss_tree -> unit) -> proof_method -> Proof.context -> int -> tactic
val trace: bool Config.T
- val setup: theory -> theory
exception Failure of string;
end
@@ -50,8 +49,7 @@
val pow2 = rat_pow rat_2;
val pow10 = rat_pow rat_10;
-val (trace, setup_trace) = Attrib.config_bool "sos_trace" (K false);
-val setup = setup_trace;
+val trace = Attrib.setup_config_bool @{binding sos_trace} (K false);
exception Sanity;
--- a/src/HOL/Meson.thy Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Meson.thy Mon May 02 17:43:42 2011 +0200
@@ -192,10 +192,7 @@
use "Tools/Meson/meson_clausify.ML"
use "Tools/Meson/meson_tactic.ML"
-setup {*
- Meson.setup
- #> Meson_Tactic.setup
-*}
+setup {* Meson_Tactic.setup *}
hide_const (open) COMBI COMBK COMBB COMBC COMBS skolem
hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD
--- a/src/HOL/Metis.thy Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Metis.thy Mon May 02 17:43:42 2011 +0200
@@ -63,10 +63,7 @@
use "Tools/Metis/metis_reconstruct.ML"
use "Tools/Metis/metis_tactics.ML"
-setup {*
- Metis_Reconstruct.setup
- #> Metis_Tactics.setup
-*}
+setup {* Metis_Tactics.setup *}
hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select
hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
--- a/src/HOL/Mirabelle/Mirabelle.thy Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Mirabelle/Mirabelle.thy Mon May 02 17:43:42 2011 +0200
@@ -14,8 +14,6 @@
ML {* Toplevel.add_hook Mirabelle.step_hook *}
-setup Mirabelle.setup
-
ML {*
signature MIRABELLE_ACTION =
sig
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Mon May 02 17:43:42 2011 +0200
@@ -9,7 +9,6 @@
val timeout : int Config.T
val start_line : int Config.T
val end_line : int Config.T
- val setup : theory -> theory
(*core*)
type init_action = int -> theory -> theory
@@ -43,12 +42,10 @@
(* Mirabelle configuration *)
-val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" (K "")
-val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" (K 30)
-val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" (K 0)
-val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" (K ~1)
-
-val setup = setup1 #> setup2 #> setup3 #> setup4
+val logfile = Attrib.setup_config_string @{binding mirabelle_logfile} (K "")
+val timeout = Attrib.setup_config_int @{binding mirabelle_timeout} (K 30)
+val start_line = Attrib.setup_config_int @{binding mirabelle_start_line} (K 0)
+val end_line = Attrib.setup_config_int @{binding mirabelle_end_line} (K ~1)
(* Mirabelle core *)
--- a/src/HOL/Nominal/nominal_thmdecls.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Mon May 02 17:43:42 2011 +0200
@@ -42,8 +42,7 @@
(* equality-lemma can be derived. *)
exception EQVT_FORM of string
-val (nominal_eqvt_debug, setup_nominal_eqvt_debug) =
- Attrib.config_bool "nominal_eqvt_debug" (K false);
+val nominal_eqvt_debug = Attrib.setup_config_bool @{binding nominal_eqvt_debug} (K false);
fun tactic ctxt (msg, tac) =
if Config.get ctxt nominal_eqvt_debug
@@ -170,7 +169,6 @@
val get_eqvt_thms = Context.Proof #> Data.get;
val setup =
- setup_nominal_eqvt_debug #>
Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del)
"equivariance theorem declaration" #>
Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
--- a/src/HOL/Sledgehammer.thy Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Sledgehammer.thy Mon May 02 17:43:42 2011 +0200
@@ -19,9 +19,6 @@
"Tools/Sledgehammer/sledgehammer_isar.ML"
begin
-setup {*
- Sledgehammer_Provers.setup
- #> Sledgehammer_Isar.setup
-*}
+setup {* Sledgehammer_Isar.setup *}
end
--- a/src/HOL/Tools/Meson/meson.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Mon May 02 17:43:42 2011 +0200
@@ -40,19 +40,17 @@
val make_meta_clause: thm -> thm
val make_meta_clauses: thm list -> thm list
val meson_tac: Proof.context -> thm list -> int -> tactic
- val setup : theory -> theory
end
structure Meson : MESON =
struct
-val (trace, trace_setup) = Attrib.config_bool "meson_trace" (K false)
+val trace = Attrib.setup_config_bool @{binding meson_trace} (K false)
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
val max_clauses_default = 60
-val (max_clauses, max_clauses_setup) =
- Attrib.config_int "meson_max_clauses" (K max_clauses_default)
+val max_clauses = Attrib.setup_config_int @{binding meson_max_clauses} (K max_clauses_default)
(*No known example (on 1-5-2007) needs even thirty*)
val iter_deepen_limit = 50;
@@ -738,8 +736,4 @@
name_thms "MClause#"
(distinct Thm.eq_thm_prop (map make_meta_clause ths));
-val setup =
- trace_setup
- #> max_clauses_setup
-
end;
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon May 02 17:43:42 2011 +0200
@@ -23,7 +23,6 @@
-> (Metis_Thm.thm * thm) list
val discharge_skolem_premises :
Proof.context -> (thm * term) option list -> thm -> thm
- val setup : theory -> theory
end;
structure Metis_Reconstruct : METIS_RECONSTRUCT =
@@ -31,8 +30,8 @@
open Metis_Translate
-val (trace, trace_setup) = Attrib.config_bool "metis_trace" (K false)
-val (verbose, verbose_setup) = Attrib.config_bool "metis_verbose" (K true)
+val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
+val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
fun verbose_warning ctxt msg =
@@ -897,6 +896,4 @@
\Error when discharging Skolem assumptions.")
end
-val setup = trace_setup #> verbose_setup
-
end;
--- a/src/HOL/Tools/Metis/metis_tactics.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon May 02 17:43:42 2011 +0200
@@ -25,9 +25,8 @@
open Metis_Translate
open Metis_Reconstruct
-val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true)
-val (new_skolemizer, new_skolemizer_setup) =
- Attrib.config_bool "metis_new_skolemizer" (K false)
+val type_lits = Attrib.setup_config_bool @{binding metis_type_lits} (K true)
+val new_skolemizer = Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
@@ -190,9 +189,7 @@
end)))
val setup =
- type_lits_setup
- #> new_skolemizer_setup
- #> method @{binding metis} HO "Metis for FOL/HOL problems"
+ method @{binding metis} HO "Metis for FOL/HOL problems"
#> method @{binding metisF} FO "Metis for FOL problems"
#> method @{binding metisFT} FT
"Metis for FOL/HOL problems with fully-typed translation"
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon May 02 17:43:42 2011 +0200
@@ -1570,12 +1570,11 @@
(* values_timeout configuration *)
-val (values_timeout, setup_values_timeout) = Attrib.config_real "values_timeout" (K 20.0)
+val values_timeout = Attrib.setup_config_real @{binding values_timeout} (K 20.0)
val setup = PredData.put (Graph.empty) #>
Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro)
"adding alternative introduction rules for code generation of inductive predicates"
- #> setup_values_timeout
(* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
(* FIXME ... this is important to avoid changing the background theory below *)
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon May 02 17:43:42 2011 +0200
@@ -28,20 +28,11 @@
(** dynamic options **)
-val (smart_quantifier, setup_smart_quantifier) =
- Attrib.config_bool "quickcheck_smart_quantifier" (K true)
-
-val (fast, setup_fast) =
- Attrib.config_bool "quickcheck_fast" (K false)
-
-val (bounded_forall, setup_bounded_forall) =
- Attrib.config_bool "quickcheck_bounded_forall" (K false)
-
-val (full_support, setup_full_support) =
- Attrib.config_bool "quickcheck_full_support" (K true)
-
-val (quickcheck_pretty, setup_quickcheck_pretty) =
- Attrib.config_bool "quickcheck_pretty" (K true)
+val smart_quantifier = Attrib.setup_config_bool @{binding quickcheck_smart_quantifier} (K true)
+val fast = Attrib.setup_config_bool @{binding quickcheck_fast} (K false)
+val bounded_forall = Attrib.setup_config_bool @{binding quickcheck_bounded_forall} (K false)
+val full_support = Attrib.setup_config_bool @{binding quickcheck_full_support} (K true)
+val quickcheck_pretty = Attrib.setup_config_bool @{binding quickcheck_pretty} (K true)
(** general term functions **)
@@ -508,11 +499,6 @@
(((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype))
#> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
(((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*)
- #> setup_smart_quantifier
- #> setup_full_support
- #> setup_fast
- #> setup_bounded_forall
- #> setup_quickcheck_pretty
#> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
#> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
#> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs));
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon May 02 17:43:42 2011 +0200
@@ -18,8 +18,7 @@
(* configurations *)
-val (finite_functions, setup_finite_functions) =
- Attrib.config_bool "quickcheck_finite_functions" (K true)
+val finite_functions = Attrib.setup_config_bool @{binding quickcheck_finite_functions} (K true)
(* narrowing specific names and types *)
@@ -208,7 +207,6 @@
val setup =
Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
(((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
- #> setup_finite_functions
#> Context.theory_map
(Quickcheck.add_generator ("narrowing", compile_generator_expr))
--- a/src/HOL/Tools/SMT/smt_config.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML Mon May 02 17:43:42 2011 +0200
@@ -23,12 +23,10 @@
(*options*)
val oracle: bool Config.T
val datatypes: bool Config.T
- val timeoutN: string
val timeout: real Config.T
val random_seed: int Config.T
val fixed: bool Config.T
val verbose: bool Config.T
- val traceN: string
val trace: bool Config.T
val trace_used_facts: bool Config.T
val monomorph_limit: int Config.T
@@ -149,75 +147,21 @@
(* options *)
-val oracleN = "smt_oracle"
-val (oracle, setup_oracle) = Attrib.config_bool oracleN (K true)
-
-val datatypesN = "smt_datatypes"
-val (datatypes, setup_datatypes) = Attrib.config_bool datatypesN (K false)
-
-val timeoutN = "smt_timeout"
-val (timeout, setup_timeout) = Attrib.config_real timeoutN (K 30.0)
-
-val random_seedN = "smt_random_seed"
-val (random_seed, setup_random_seed) = Attrib.config_int random_seedN (K 1)
-
-val fixedN = "smt_fixed"
-val (fixed, setup_fixed) = Attrib.config_bool fixedN (K false)
-
-val verboseN = "smt_verbose"
-val (verbose, setup_verbose) = Attrib.config_bool verboseN (K true)
-
-val traceN = "smt_trace"
-val (trace, setup_trace) = Attrib.config_bool traceN (K false)
-
-val trace_used_factsN = "smt_trace_used_facts"
-val (trace_used_facts, setup_trace_used_facts) =
- Attrib.config_bool trace_used_factsN (K false)
-
-val monomorph_limitN = "smt_monomorph_limit"
-val (monomorph_limit, setup_monomorph_limit) =
- Attrib.config_int monomorph_limitN (K 10)
-
-val monomorph_instancesN = "smt_monomorph_instances"
-val (monomorph_instances, setup_monomorph_instances) =
- Attrib.config_int monomorph_instancesN (K 500)
-
-val monomorph_fullN = "smt_monomorph_full"
-val (monomorph_full, setup_monomorph_full) =
- Attrib.config_bool monomorph_fullN (K true)
-
-val infer_triggersN = "smt_infer_triggers"
-val (infer_triggers, setup_infer_triggers) =
- Attrib.config_bool infer_triggersN (K false)
-
-val drop_bad_factsN = "smt_drop_bad_facts"
-val (drop_bad_facts, setup_drop_bad_facts) =
- Attrib.config_bool drop_bad_factsN (K false)
-
-val filter_only_factsN = "smt_filter_only_facts"
-val (filter_only_facts, setup_filter_only_facts) =
- Attrib.config_bool filter_only_factsN (K false)
-
-val debug_filesN = "smt_debug_files"
-val (debug_files, setup_debug_files) =
- Attrib.config_string debug_filesN (K "")
-
-val setup_options =
- setup_oracle #>
- setup_datatypes #>
- setup_timeout #>
- setup_random_seed #>
- setup_fixed #>
- setup_trace #>
- setup_verbose #>
- setup_monomorph_limit #>
- setup_monomorph_instances #>
- setup_monomorph_full #>
- setup_infer_triggers #>
- setup_drop_bad_facts #>
- setup_filter_only_facts #>
- setup_trace_used_facts #>
- setup_debug_files
+val oracle = Attrib.setup_config_bool @{binding smt_oracle} (K true)
+val datatypes = Attrib.setup_config_bool @{binding smt_datatypes} (K false)
+val timeout = Attrib.setup_config_real @{binding smt_timeout} (K 30.0)
+val random_seed = Attrib.setup_config_int @{binding smt_random_seed} (K 1)
+val fixed = Attrib.setup_config_bool @{binding smt_fixed} (K false)
+val verbose = Attrib.setup_config_bool @{binding smt_verbose} (K true)
+val trace = Attrib.setup_config_bool @{binding smt_trace} (K false)
+val trace_used_facts = Attrib.setup_config_bool @{binding smt_trace_used_facts} (K false)
+val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10)
+val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500)
+val monomorph_full = Attrib.setup_config_bool @{binding smt_monomorph_full} (K true)
+val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false)
+val drop_bad_facts = Attrib.setup_config_bool @{binding smt_drop_bad_facts} (K false)
+val filter_only_facts = Attrib.setup_config_bool @{binding smt_filter_only_facts} (K false)
+val debug_files = Attrib.setup_config_string @{binding smt_debug_files} (K "")
(* diagnostics *)
@@ -269,7 +213,6 @@
val setup =
setup_solver #>
- setup_options #>
setup_certificates
fun print_setup ctxt =
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML Mon May 02 17:43:42 2011 +0200
@@ -43,7 +43,7 @@
else if String.isPrefix unknown line then SMT_Solver.Unknown
else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^
quote solver_name ^ " failed. Enable SMT tracing by setting the " ^
- "configuration option " ^ quote SMT_Config.traceN ^ " and " ^
+ "configuration option " ^ quote (Config.name_of SMT_Config.trace) ^ " and " ^
"see the trace for details."))
fun on_first_line test_outcome solver_name lines =
--- a/src/HOL/Tools/SMT/smt_solver.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Mon May 02 17:43:42 2011 +0200
@@ -350,7 +350,7 @@
| SMT_Failure.SMT (fail as SMT_Failure.Time_Out) =>
error ("SMT: Solver " ^ quote (SMT_Config.solver_of ctxt) ^ ": " ^
SMT_Failure.string_of_failure ctxt fail ^ " (setting the " ^
- "configuration option " ^ SMT_Config.timeoutN ^ " might help)")
+ "configuration option " ^ quote (Config.name_of SMT_Config.timeout) ^ " might help)")
| SMT_Failure.SMT fail => error (str_of ctxt fail)
fun tag_rules thms = map_index (apsnd (pair NONE)) thms
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 02 17:43:42 2011 +0200
@@ -96,7 +96,6 @@
val running_provers : unit -> unit
val messages : int option -> unit
val get_prover : Proof.context -> bool -> string -> prover
- val setup : theory -> theory
end;
structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS =
@@ -272,15 +271,15 @@
(* configuration attributes *)
-val (dest_dir, dest_dir_setup) =
- Attrib.config_string "sledgehammer_dest_dir" (K "")
+val dest_dir =
+ Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
(* Empty string means create files in Isabelle's temporary files directory. *)
-val (problem_prefix, problem_prefix_setup) =
- Attrib.config_string "sledgehammer_problem_prefix" (K "prob")
+val problem_prefix =
+ Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
-val (measure_run_time, measure_run_time_setup) =
- Attrib.config_bool "sledgehammer_measure_run_time" (K false)
+val measure_run_time =
+ Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false)
fun with_path cleanup after f path =
Exn.capture f path
@@ -804,9 +803,4 @@
error ("No such prover: " ^ name ^ ".")
end
-val setup =
- dest_dir_setup
- #> problem_prefix_setup
- #> measure_run_time_setup
-
end;
--- a/src/HOL/Tools/inductive_codegen.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Mon May 02 17:43:42 2011 +0200
@@ -862,10 +862,10 @@
NONE => deepen bound f (i + 1)
| SOME x => SOME x);
-val (depth_bound, setup_depth_bound) = Attrib.config_int "ind_quickcheck_depth" (K 10);
-val (depth_start, setup_depth_start) = Attrib.config_int "ind_quickcheck_depth_start" (K 1);
-val (random_values, setup_random_values) = Attrib.config_int "ind_quickcheck_random" (K 5);
-val (size_offset, setup_size_offset) = Attrib.config_int "ind_quickcheck_size_offset" (K 0);
+val depth_bound = Attrib.setup_config_int @{binding ind_quickcheck_depth} (K 10);
+val depth_start = Attrib.setup_config_int @{binding ind_quickcheck_depth_start} (K 1);
+val random_values = Attrib.setup_config_int @{binding ind_quickcheck_random} (K 5);
+val size_offset = Attrib.setup_config_int @{binding ind_quickcheck_size_offset} (K 0);
fun test_term ctxt [(t, [])] =
let
@@ -925,10 +925,6 @@
error "Compilation of multiple instances is not supported by tester SML_inductive";
val quickcheck_setup =
- setup_depth_bound #>
- setup_depth_start #>
- setup_random_values #>
- setup_size_offset #>
Context.theory_map (Quickcheck.add_generator ("SML_inductive", test_term));
end;
--- a/src/HOL/Tools/lin_arith.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/HOL/Tools/lin_arith.ML Mon May 02 17:43:42 2011 +0200
@@ -99,8 +99,8 @@
{splits = splits, inj_consts = update (op =) c inj_consts,
discrete = discrete});
-val (split_limit, setup_split_limit) = Attrib.config_int "linarith_split_limit" (K 9);
-val (neq_limit, setup_neq_limit) = Attrib.config_int "linarith_neq_limit" (K 9);
+val split_limit = Attrib.setup_config_int @{binding linarith_split_limit} (K 9);
+val neq_limit = Attrib.setup_config_int @{binding linarith_neq_limit} (K 9);
structure LA_Data =
@@ -905,7 +905,6 @@
(add_arith_facts #> Fast_Arith.cut_lin_arith_tac)))
val global_setup =
- setup_split_limit #> setup_neq_limit #>
Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))
"declaration of split rules for arithmetic procedure" #>
Method.setup @{binding linarith}
--- a/src/Provers/blast.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/Provers/blast.ML Mon May 02 17:43:42 2011 +0200
@@ -1269,7 +1269,8 @@
(*Public version with fixed depth*)
fun depth_tac cs lim i st = timing_depth_tac (Timing.start ()) cs lim i st;
-val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" (K 20);
+val (depth_limit, setup_depth_limit) =
+ Attrib.config_int_global @{binding blast_depth_limit} (K 20);
fun blast_tac cs i st =
((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit)
--- a/src/Pure/Isar/attrib.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/Pure/Isar/attrib.ML Mon May 02 17:43:42 2011 +0200
@@ -36,15 +36,26 @@
val multi_thm: thm list context_parser
val print_configs: Proof.context -> unit
val internal: (morphism -> attribute) -> src
- val config_bool: bstring -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
- val config_int: bstring -> (Context.generic -> int) -> int Config.T * (theory -> theory)
- val config_real: bstring -> (Context.generic -> real) -> real Config.T * (theory -> theory)
- val config_string: bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
- val config_bool_global: bstring -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
- val config_int_global: bstring -> (Context.generic -> int) -> int Config.T * (theory -> theory)
- val config_real_global: bstring -> (Context.generic -> real) -> real Config.T * (theory -> theory)
- val config_string_global:
- bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
+ val config_bool: Binding.binding ->
+ (Context.generic -> bool) -> bool Config.T * (theory -> theory)
+ val config_int: Binding.binding ->
+ (Context.generic -> int) -> int Config.T * (theory -> theory)
+ val config_real: Binding.binding ->
+ (Context.generic -> real) -> real Config.T * (theory -> theory)
+ val config_string: Binding.binding ->
+ (Context.generic -> string) -> string Config.T * (theory -> theory)
+ val config_bool_global: Binding.binding ->
+ (Context.generic -> bool) -> bool Config.T * (theory -> theory)
+ val config_int_global: Binding.binding ->
+ (Context.generic -> int) -> int Config.T * (theory -> theory)
+ val config_real_global: Binding.binding ->
+ (Context.generic -> real) -> real Config.T * (theory -> theory)
+ val config_string_global: Binding.binding ->
+ (Context.generic -> string) -> string Config.T * (theory -> theory)
+ val setup_config_bool: Binding.binding -> (Context.generic -> bool) -> bool Config.T
+ val setup_config_int: Binding.binding -> (Context.generic -> int) -> int Config.T
+ val setup_config_string: Binding.binding -> (Context.generic -> string) -> string Config.T
+ val setup_config_real: Binding.binding -> (Context.generic -> real) -> real Config.T
end;
structure Attrib: ATTRIB =
@@ -366,34 +377,53 @@
let val config_type = Config.get_global thy config
in scan_value config_type >> (K o Thm.declaration_attribute o K o Config.put_generic config) end;
-in
-
-fun register_config config thy =
- let
- val bname = Config.name_of config;
- val name = Sign.full_bname thy bname;
- in
+fun register binding config thy =
+ let val name = Sign.full_name thy binding in
thy
- |> setup (Binding.name bname) (Scan.lift (scan_config thy config) >> Morphism.form)
- "configuration option"
+ |> setup binding (Scan.lift (scan_config thy config) >> Morphism.form) "configuration option"
|> Configs.map (Symtab.update (name, config))
end;
-fun declare_config make coerce global name default =
+fun declare make coerce global binding default =
let
+ val name = Binding.name_of binding;
val config_value = Config.declare_generic {global = global} name (make o default);
val config = coerce config_value;
- in (config, register_config config_value) end;
+ in (config, register binding config_value) end;
+
+in
+
+val config_bool = declare Config.Bool Config.bool false;
+val config_int = declare Config.Int Config.int false;
+val config_real = declare Config.Real Config.real false;
+val config_string = declare Config.String Config.string false;
+
+val config_bool_global = declare Config.Bool Config.bool true;
+val config_int_global = declare Config.Int Config.int true;
+val config_real_global = declare Config.Real Config.real true;
+val config_string_global = declare Config.String Config.string true;
+
+fun register_config config = register (Binding.name (Config.name_of config)) config;
+
+end;
-val config_bool = declare_config Config.Bool Config.bool false;
-val config_int = declare_config Config.Int Config.int false;
-val config_real = declare_config Config.Real Config.real false;
-val config_string = declare_config Config.String Config.string false;
+
+(* implicit setup *)
+
+local
-val config_bool_global = declare_config Config.Bool Config.bool true;
-val config_int_global = declare_config Config.Int Config.int true;
-val config_real_global = declare_config Config.Real Config.real true;
-val config_string_global = declare_config Config.String Config.string true;
+fun setup_config declare_config binding default =
+ let
+ val (config, setup) = declare_config binding default;
+ val _ = Context.>> (Context.map_theory setup);
+ in config end;
+
+in
+
+val setup_config_bool = setup_config config_bool;
+val setup_config_int = setup_config config_int;
+val setup_config_string = setup_config config_string;
+val setup_config_real = setup_config config_real;
end;
--- a/src/Pure/Isar/method.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/Pure/Isar/method.ML Mon May 02 17:43:42 2011 +0200
@@ -218,7 +218,7 @@
(* rule etc. -- single-step refinements *)
-val (rule_trace, rule_trace_setup) = Attrib.config_bool "rule_trace" (fn _ => false);
+val rule_trace = Attrib.setup_config_bool (Binding.name "rule_trace") (fn _ => false);
fun trace ctxt rules =
if Config.get ctxt rule_trace andalso not (null rules) then
@@ -441,8 +441,7 @@
(* theory setup *)
val _ = Context.>> (Context.map_theory
- (rule_trace_setup #>
- setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #>
+ (setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #>
setup (Binding.name "succeed") (Scan.succeed (K succeed)) "succeed" #>
setup (Binding.name "-") (Scan.succeed (K insert_facts))
"do nothing (insert current facts only)" #>
--- a/src/Pure/Thy/thy_output.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/Pure/Thy/thy_output.ML Mon May 02 17:43:42 2011 +0200
@@ -51,14 +51,11 @@
val source_default = Unsynchronized.ref false;
val break_default = Unsynchronized.ref false;
-val (display, setup_display) = Attrib.config_bool "thy_output_display" (fn _ => ! display_default);
-val (quotes, setup_quotes) = Attrib.config_bool "thy_output_quotes" (fn _ => ! quotes_default);
-val (indent, setup_indent) = Attrib.config_int "thy_output_indent" (fn _ => ! indent_default);
-val (source, setup_source) = Attrib.config_bool "thy_output_source" (fn _ => ! source_default);
-val (break, setup_break) = Attrib.config_bool "thy_output_break" (fn _ => ! break_default);
-
-val _ = Context.>> (Context.map_theory
- (setup_display #> setup_quotes #> setup_indent #> setup_source #> setup_break));
+val display = Attrib.setup_config_bool (Binding.name "thy_output_display") (fn _ => ! display_default);
+val quotes = Attrib.setup_config_bool (Binding.name "thy_output_quotes") (fn _ => ! quotes_default);
+val indent = Attrib.setup_config_int (Binding.name "thy_output_indent") (fn _ => ! indent_default);
+val source = Attrib.setup_config_bool (Binding.name "thy_output_source") (fn _ => ! source_default);
+val break = Attrib.setup_config_bool (Binding.name "thy_output_break") (fn _ => ! break_default);
structure Wrappers = Proof_Data
--- a/src/Tools/quickcheck.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/Tools/quickcheck.ML Mon May 02 17:43:42 2011 +0200
@@ -132,21 +132,16 @@
if expect1 = expect2 then expect1 else No_Expectation
(* quickcheck configuration -- default parameters, test generators *)
-val (tester, setup_tester) = Attrib.config_string "quickcheck_tester" (K "")
-val (size, setup_size) = Attrib.config_int "quickcheck_size" (K 10)
-val (iterations, setup_iterations) = Attrib.config_int "quickcheck_iterations" (K 100)
-val (no_assms, setup_no_assms) = Attrib.config_bool "quickcheck_no_assms" (K false)
-val (report, setup_report) = Attrib.config_bool "quickcheck_report" (K true)
-val (timing, setup_timing) = Attrib.config_bool "quickcheck_timing" (K false)
-val (quiet, setup_quiet) = Attrib.config_bool "quickcheck_quiet" (K false)
-val (timeout, setup_timeout) = Attrib.config_real "quickcheck_timeout" (K 30.0)
-val (finite_types, setup_finite_types) = Attrib.config_bool "quickcheck_finite_types" (K true)
-val (finite_type_size, setup_finite_type_size) =
- Attrib.config_int "quickcheck_finite_type_size" (K 3)
-
-val setup_config =
- setup_tester #> setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_timing
- #> setup_quiet #> setup_timeout #> setup_finite_types #> setup_finite_type_size
+val tester = Attrib.setup_config_string @{binding quickcheck_tester} (K "")
+val size = Attrib.setup_config_int @{binding quickcheck_size} (K 10)
+val iterations = Attrib.setup_config_int @{binding quickcheck_iterations} (K 100)
+val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
+val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true)
+val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false)
+val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false)
+val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
+val finite_types = Attrib.setup_config_bool @{binding quickcheck_finite_types} (K true)
+val finite_type_size = Attrib.setup_config_int @{binding quickcheck_finite_type_size} (K 3)
datatype test_params = Test_Params of
{default_type: typ list, expect : expectation};
@@ -536,7 +531,6 @@
end
val setup = Auto_Tools.register_tool (auto, auto_quickcheck)
- #> setup_config
(* Isar commands *)
--- a/src/Tools/subtyping.ML Mon May 02 15:13:10 2011 +0200
+++ b/src/Tools/subtyping.ML Mon May 02 17:43:42 2011 +0200
@@ -711,8 +711,7 @@
(* term check *)
-val (coercion_enabled, coercion_enabled_setup) =
- Attrib.config_bool "coercion_enabled" (K false);
+val coercion_enabled = Attrib.setup_config_bool @{binding coercion_enabled} (K false);
val add_term_check =
Syntax.add_term_check ~100 "coercions"
@@ -820,7 +819,6 @@
(* theory setup *)
val setup =
- coercion_enabled_setup #>
Context.theory_map add_term_check #>
Attrib.setup @{binding coercion}
(Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t))))