[isabelle] Add a definition to the simplifier

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.