Am 13.02.2014 um 13:35 schrieb Lawrence Paulson <[email protected]>:
> I know it was a problem for machine learning that a free variable in a goal
> (x say) might appear with multiple types in a problem set. This is connected
> with the issue you’re describing now. I assume that that was solved somehow.
All I'm trying to say is that
lemma "n ~= Suc n"
using [[metis_trace]] by (metis Suc_n_not_n)
and
lemma "x ~= Suc x"
using [[metis_trace]] by (metis Suc_n_not_n)
generate slightly different clauses at the Metis level, as can be seen in the
trace. One gets
|- v_n = c_Nat_OSuc v_n
vs.
|- v_x = c_Nat_OSuc v_x
To Metis, "v_n" and "v_x" are nullary function symbols (constants). Some of its
heuristics are influenced by the concrete names, or at least their relative
ordering. So it mgiht be very fast on the first one and very slow on the second
one.
Jasmin
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
