doc-src/IsarRef/Thy/Generic.thy
changeset 42655 eb95e2f3b218
parent 42651 e3fdb7c96be5
child 42704 3f19e324ff59
     1.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Tue May 03 15:37:17 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Tue May 03 16:00:29 2011 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  
     1.5  chapter {* Generic tools and packages \label{ch:gen-tools} *}
     1.6  
     1.7 -section {* Configuration options *}
     1.8 +section {* Configuration options \label{sec:config} *}
     1.9  
    1.10  text {* Isabelle/Pure maintains a record of named configuration
    1.11    options within the theory or proof context, with values of type
    1.12 @@ -14,9 +14,18 @@
    1.13    are easily avoided.  The user may change the value of a
    1.14    configuration option by means of an associated attribute of the same
    1.15    name.  This form of context declaration works particularly well with
    1.16 -  commands such as @{command "declare"} or @{command "using"}.
    1.17 +  commands such as @{command "declare"} or @{command "using"} like
    1.18 +  this:
    1.19 +*}
    1.20 +
    1.21 +declare [[show_main_goal = false]]
    1.22  
    1.23 -  For historical reasons, some tools cannot take the full proof
    1.24 +notepad
    1.25 +begin
    1.26 +  note [[show_main_goal = true]]
    1.27 +end
    1.28 +
    1.29 +text {* For historical reasons, some tools cannot take the full proof
    1.30    context into account and merely refer to the background theory.
    1.31    This is accommodated by configuration options being declared as
    1.32    ``global'', which may not be changed within a local context.