98 and parse_expr xs =

    98 and parse_expr xs =

    99   (parse_factor --| OuterParse.$$$ "+" -- parse_expr >> Add 

    99   (parse_factor --| OuterParse.$$$ "+" -- parse_expr >> Add 

   100    || parse_factor) xs*}

   100    || parse_factor) xs*}

   101 

   101 

   102 

   102 

   104   The axiom rule can be implemented with the function @{ML atac}. The other

   106   The axiom rule can be implemented with the function @{ML atac}. The other

   105   rules correspond to the theorems:

   107   rules correspond to the theorems:

   106 

   108 

   107   \begin{center}

   109   \begin{center}

   108   \begin{tabular}{cc}

   110   \begin{tabular}{cc}

   240 text {*

   242 text {*

   241   The following code assumes the function @{ML dest_sum} from the previous

   243   The following code assumes the function @{ML dest_sum} from the previous

   242   exercise.

   244   exercise.

   243 *}

   245 *}

   244 

   246 

   246 let

   248 let

   247   val trm = Thm.term_of ctrm

   249   val trm = Thm.term_of ctrm

   248 in

   250 in

   249   case trm of

   251   case trm of

   250      @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => 

   252      @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => 

   271   \begin{minipage}{\textwidth}

   273   \begin{minipage}{\textwidth}

   272   @{subgoals [display]}

   274   @{subgoals [display]}

   273   \end{minipage}\bigskip

   275   \end{minipage}\bigskip

   274 *}(*<*)oops(*>*)

   276 *}(*<*)oops(*>*)

   275 

   277 

   277 

   279 

   278 text {* 

   280 text {* 

   279   We use the timing function @{ML timing_wrapper} from Recipe~\ref{rec:timing}.

   281   We use the timing function @{ML timing_wrapper} from Recipe~\ref{rec:timing}.

   280   To measure any difference between the simproc and conversion, we will create 

   282   To measure any difference between the simproc and conversion, we will create 

   281   mechanically terms involving additions and then set up a goal to be 

   283   mechanically terms involving additions and then set up a goal to be 

   325 ML{*local

   327 ML{*local

   326   fun mk_tac tac = 

   328   fun mk_tac tac = 

   327         timing_wrapper (EVERY1 [tac, K (Skip_Proof.cheat_tac @{theory})])

   329         timing_wrapper (EVERY1 [tac, K (Skip_Proof.cheat_tac @{theory})])

   328 in

   330 in

   329   val c_tac = mk_tac (add_tac @{context}) 

   331   val c_tac = mk_tac (add_tac @{context}) 

   331 end*}

   334 end*}

   332 

   335 

   333 text {*

   336 text {*

   334   This is all we need to let the conversion run against the simproc:

   337   This is all we need to let the conversion run against the simproc:

   335 *}

   338 *}