[isabelle-dev] Forward reasoning with schematic variables?

[Steven Obua]

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