[isabelle] Add a definition to the simplifier



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.