Hi Andreas,
"taking" was actually what I was searching for, thanks! I just found it
strange to write (induct key xs rule: ...) when "key" staid the same all
the time.
cheers
chris
On 11/03/2011 12:40 PM, Andreas Lochbihler wrote:
Hi Christian,
I am not completely sure what you mean. It is
Hi Christian,
I am not completely sure what you mean. It is possible to leave key out of the
conclusion in sequences_induct.
lemma sequences_induct[case_names Nil singleton IH]:
assumes "P []" and "!!x. P [x]"
and "!!a b xs. [| key b < key a ==> P (drop_desc key b xs);
~
