1317 

  1317 

  1318 text {* 

  1318 text {* 

  1319   where the function @{ML_ind  rule_attribute in Thm} expects a function taking a 

  1319   where the function @{ML_ind  rule_attribute in Thm} expects a function taking a 

  1320   context (which we ignore in the code above) and a theorem (@{text thm}), and 

  1320   context (which we ignore in the code above) and a theorem (@{text thm}), and 

  1321   returns another theorem (namely @{text thm} resolved with the theorem 

  1321   returns another theorem (namely @{text thm} resolved with the theorem 

  1323   is explained in Section~\ref{sec:simpletacs}). The function 

  1323   is explained in Section~\ref{sec:simpletacs}). The function 

  1324   @{ML rule_attribute in Thm} then returns  an attribute.

  1324   @{ML rule_attribute in Thm} then returns  an attribute.

  1325 

  1325 

  1326   Before we can use the attribute, we need to set it up. This can be done

  1326   Before we can use the attribute, we need to set it up. This can be done

  1327   using the Isabelle command \isacommand{attribute\_setup} as follows:

  1327   using the Isabelle command \isacommand{attribute\_setup} as follows: