Re: [isabelle] Introducing a variable from a constant



> lemma empty_unaccepted[simp]: "¬ (accepted prods nt [])"
> 
The following should work:

  apply (rule)
  apply (drule empty_unaccepted_helper)
  by auto


Peter







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