Hi, until shortly before the Isabelle2007 release the following line worked:
lemmas find_simp = While_simp[where continue="(\<lambda> x. ?f x \<noteq> x)", simplified find_def[symmetric]] Now it complains that the schematic variable ?f is not allowed. This variable occurs in While_simp, too, and I want to specialize While_simp by setting one schematic variable of the theorem to a term that contains another schematic variable of the theorem. Is there an alternative way of doing this? Thanks, Steven
