[isabelle-dev] Forward reasoning with schematic variables?

Steven Obua obua at in.tum.de
Tue Dec 4 15:17:22 CET 2007


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?



More information about the isabelle-dev mailing list