[isabelle] Strange variable binding on obtains - long-goal format
referring to Isaballe 2011-1
I just encountered some (in my opinion strange) behavior of the obtains
obtains sym where "sym = w"
sym = (w\<Colon>('a \<times> 'a \<Rightarrow> bool) \<Rightarrow>
bool) \<Longrightarrow> thesis\<Colon>bool
That is, sym is recognized as a constant (Relation.sym) here, instead of
a bound variable, as I would expect.
Is there a workaround, i.e., can I use a name declared as a constant
somewhere in an obtains-goal?
Adding a "fixes sym" to the lemma results in a "duplicate fixed
If this behavior is intended, is there any reason for silently ignoring
the variable binding given by the user, not even issuing a warning?
This archive was generated by a fusion of
Pipermail (Mailman edition) and