[isabelle-dev] Forward reasoning with schematic variables?
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