[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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and