src/HOLCF/IOA/NTP/Impl.ML
changeset 16734 2c76db916c51
parent 15408 6001135caa91
child 17244 0b2ff9541727
equal deleted inserted replaced
16733:236dfafbeb63 16734:2c76db916c51
   174 
   174 
   175   (* 4 *)
   175   (* 4 *)
   176   by (forward_tac [rewrite_rule [Impl.inv1_def]
   176   by (forward_tac [rewrite_rule [Impl.inv1_def]
   177                                 (inv1 RS invariantE) RS conjunct1] 1);
   177                                 (inv1 RS invariantE) RS conjunct1] 1);
   178   by (tac2 1);
   178   by (tac2 1);
   179   by (arith_tac 1);
       
   180 
   179 
   181   (* 3 *)
   180   (* 3 *)
   182   by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1);
   181   by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1);
   183 
   182 
   184   by (tac2 1);
   183   by (tac2 1);