1145 section {* Setups (TBD) *}

  1146 

  1147 text {*

  1148   In the previous section we used \isacommand{setup} in order to make

  1149   a theorem attribute known to Isabelle. What happens behind the scenes

  1150   is that \isacommand{setup} expects a function of type 

  1151   @{ML_type "theory -> theory"}: the input theory is the current theory and the 

  1152   output the theory where the theory attribute has been stored.

  1153   

  1154   This is a fundamental principle in Isabelle. A similar situation occurs 

  1155   for example with declaring constants. The function that declares a 

  1156   constant on the ML-level is @{ML Sign.add_consts_i}. 

  1157   If you write\footnote{Recall that ML-code  needs to be 

  1158   enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} 

  1159 *}  

  1160 

  1161 ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *}

  1162 

  1163 text {*

  1164   for declaring the constant @{text "BAR"} with type @{typ nat} and 

  1165   run the code, then you indeed obtain a theory as result. But if you 

  1166   query the constant on the Isabelle level using the command \isacommand{term}

  1167 

  1168   \begin{isabelle}

  1169   \isacommand{term}~@{text [quotes] "BAR"}\\

  1170   @{text "> \"BAR\" :: \"'a\""}

  1171   \end{isabelle}

  1172 

  1173   you do not obtain a constant of type @{typ nat}, but a free variable (printed in 

  1174   blue) of polymorphic type. The problem is that the ML-expression above did 

  1175   not register the declaration with the current theory. This is what the command

  1176   \isacommand{setup} is for. The constant is properly declared with

  1177 *}

  1178 

  1179 setup %gray {* Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] *}

  1180 

  1181 text {* 

  1182   Now 

  1183   

  1184   \begin{isabelle}

  1185   \isacommand{term}~@{text [quotes] "BAR"}\\

  1186   @{text "> \"BAR\" :: \"nat\""}

  1187   \end{isabelle}

  1188 

  1189   returns a (black) constant with the type @{typ nat}.

  1190 

  1191   A similar command is \isacommand{local\_setup}, which expects a function

  1192   of type @{ML_type "local_theory -> local_theory"}. Later on we will also

  1193   use the commands \isacommand{method\_setup} for installing methods in the

  1194   current theory and \isacommand{simproc\_setup} for adding new simprocs to

  1195   the current simpset.

  1196 *}

  1197 

  1275   An alternative for setting up an attribute is the function @{ML Attrib.setup}.

  1276   So instead of using \isacommand{attribute\_setup}, you can also set up the

  1277   attribute as follows:

  1278 *}

  1279 

  1280 ML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)

  1281   "applying the sym rule" *}

  1282 

  1283 text {*

  1284   This gives a function from @{ML_type "Context.theory -> Context.theory"}, which

  1285   can be used for example with \isacommand{setup}.

  1286