31 let 

    31 let 

    32   val t_start = start_timing ();

    32   val t_start = start_timing ();

    33   val res = tac st;

    33   val res = tac st;

    34   val t_end = end_timing t_start;

    34   val t_end = end_timing t_start;

    35 in

    35 in

    37 end*}

    37 end*}

    38 

    38 

    39 text {*

    39 text {*

    40   Note that this function, in addition to a tactic, also takes a state @{text

    40   Note that this function, in addition to a tactic, also takes a state @{text

    41   "st"} as argument and applies this state to the tactic (Line 4). The reason is that

    41   "st"} as argument and applies this state to the tactic (Line 4). The reason is that