Re: [isabelle] limiting unfolding using definitions



I have a goal "f <= g" where f, g:: A => B => C.
I want to unfold the goal using le_fun_def only once:
"!! x . f x <= g x"

  apply (subst le_fun_def)

or, in this particular case

  apply (rule le_funI)


Alex





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