Re: [isabelle] Introducing a variable from a constant



> lemma empty_unaccepted[simp]: "¬ (accepted prods nt [])"
> proof (rule notI)
>   assume "accepted prods nt []"
>   with empty_unaccepted_helper[OF this] show "False" by simp
> qed

Thanks. I used a slightly modified version of that where I didn't need
`empty_unaccepted_helper`, but rather proved the lemma directly in a
sub-proof.






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