[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"]) ;
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and