[isabelle] cut_inst_tac and insert




I have a goal of the form


 1. !!a list.
          ... list ...

When I do

apply (tactic "(cut_inst_tac [(\"x\", \"n\"), (\"y\", \"size list\")]
    linorder_less_linear 1)") ;

the goal becomes

    n < length list | n = length list | length list < n ==> (as before)

but if instead I do

  apply (insert linorder_less_linear [where x = "n" and y = "size list"]) ;

I get

 !!a lista.

          n < size list | n = size list | size list < n |]
       ==> (as before, but with list replaces by lista)

Why is this?  Is it possible (using Isar) to stop this happening?

Thanks for any help

Jeremy





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.