Re: [isabelle] Add a definition to the simplifier
definition continuous where [simp]: "continuous f = ..."
should work. Or make continuous a function (defined with "fun" rather than "definition") and it'll be added to the simplifier automatically.
On 10 Jan 2014, at 14:55, Roger H. <s57076 at hotmail.com> wrote:
> can i add a definition to the simplifier?
> means, lets say i define a predicate "continuous"
> definition continuous :: ...
> All my lemmas need this, and everytime i need to prove lemmas , i have to add as proof method "continuous_def".
> it would be nicer if this was not neccesary to drag by every time, meaning that somehow this proof method is added to the simplifier.
> how can i do this?
> Thank you!
This archive was generated by a fusion of
Pipermail (Mailman edition) and