Re: [isabelle] Add a definition to the simplifier



Something like 

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.

john

On 10 Jan 2014, at 14:55, Roger H. <s57076 at hotmail.com> wrote:

> Hi,
> 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 MHonArc.