# HG changeset patch # User wenzelm # Date 1304351022 -7200 # Node ID 613b9b589ca0bd42dfe95cc71537395ad6b691aa # Parent 8d7039b6ad7ab5f541f89eaaf7952f25a9bdd890# Parent 61a99eb5eb9dea53612cde0c0df5f9e3ffc90ed5 merged diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/IsarImplementation/Thy/Prelim.thy --- 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]] diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/IsarImplementation/Thy/document/Prelim.tex --- 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}% % diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/IsarImplementation/implementation.tex --- 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} diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/IsarRef/Makefile --- 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) diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/IsarRef/Thy/Document_Preparation.thy --- 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 "\"}~@{verbatim "*)"} nor verbatim diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/IsarRef/Thy/Generic.thy --- 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} diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/IsarRef/Thy/HOL_Specific.thy --- 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 diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/IsarRef/Thy/Proof.thy --- 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 @@ \"} 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: \"} 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} diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/IsarRef/Thy/Spec.thy --- 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} ('<' | '\') @{syntax localeexpr} equations? + @@{command sublocale} @{syntax nameref} ('<' | '\') @{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} ( '==' | '\' ) @{syntax term} + ( @{syntax name} ( '==' | '\' ) @{syntax term} ( '(' @'unchecked' ')' )? +) @'begin' - "} %% FIXME check string vs. name + "} \begin{description} diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/IsarRef/Thy/document/Document_Preparation.tex --- 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 diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/IsarRef/Thy/document/Generic.tex --- 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} diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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 diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/IsarRef/Thy/document/Proof.tex --- 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} diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/IsarRef/Thy/document/Spec.tex --- 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} diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/IsarRef/isar-ref.tex --- 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}} diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/ZF/Makefile --- 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 diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/ZF/ZF.tex --- 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. diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/ZF/logics-ZF.rai --- 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 '"' + ',') ')' ; } diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/ZF/logics-ZF.rao --- 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 -} diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/ZF/logics-ZF.tex --- 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! diff -r 8d7039b6ad7a -r 613b9b589ca0 doc-src/railsetup.sty --- 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}}} + diff -r 8d7039b6ad7a -r 613b9b589ca0 src/FOLP/IFOLP.thy --- 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 diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Library/Sum_of_Squares.thy --- 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 *} diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Library/Sum_of_Squares/sos_wrapper.ML --- 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 => diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML --- 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; diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Meson.thy --- 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 diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Metis.thy --- 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 diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Mirabelle/Mirabelle.thy --- 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 diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Mirabelle/Tools/mirabelle.ML --- 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 *) diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Nominal/nominal_thmdecls.ML --- 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) diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Sledgehammer.thy --- 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 diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Tools/Meson/meson.ML --- 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; diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Tools/Metis/metis_reconstruct.ML --- 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; diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Tools/Metis/metis_tactics.ML --- 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" diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 *) diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- 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)); diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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)) diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Tools/SMT/smt_config.ML --- 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 = diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Tools/SMT/smt_setup_solvers.ML --- 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 = diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Tools/SMT/smt_solver.ML --- 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 diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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; diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Tools/inductive_codegen.ML --- 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; diff -r 8d7039b6ad7a -r 613b9b589ca0 src/HOL/Tools/lin_arith.ML --- 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} diff -r 8d7039b6ad7a -r 613b9b589ca0 src/Provers/blast.ML --- 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) diff -r 8d7039b6ad7a -r 613b9b589ca0 src/Pure/Isar/attrib.ML --- 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; diff -r 8d7039b6ad7a -r 613b9b589ca0 src/Pure/Isar/method.ML --- 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)" #> diff -r 8d7039b6ad7a -r 613b9b589ca0 src/Pure/Thy/thy_output.ML --- 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 diff -r 8d7039b6ad7a -r 613b9b589ca0 src/Tools/quickcheck.ML --- 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 *) diff -r 8d7039b6ad7a -r 613b9b589ca0 src/Tools/subtyping.ML --- 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))))