ProgTutorial/Solutions.thy
changeset 410 2656354c7544
parent 407 aee4abd02db1
child 424 5e0a2b50707e
equal deleted inserted replaced
409:f1743ce9dbf1 410:2656354c7544
   254     | _ => Conv.all_conv ctrm
   254     | _ => Conv.all_conv ctrm
   255 end
   255 end
   256 
   256 
   257 val add_conv = More_Conv.bottom_conv add_simple_conv
   257 val add_conv = More_Conv.bottom_conv add_simple_conv
   258 
   258 
   259 fun add_tac ctxt = CONVERSION
   259 fun add_tac ctxt = CONVERSION (add_conv ctxt)*}
   260     (Conv.params_conv ~1 (fn ctxt =>
       
   261        (Conv.prems_conv ~1 (add_conv ctxt) then_conv
       
   262           Conv.concl_conv ~1 (add_conv ctxt))) ctxt)*}
       
   263 
   260 
   264 text {*
   261 text {*
   265   A test case for this conversion is as follows
   262   A test case for this conversion is as follows
   266 *}
   263 *}
   267 
   264