Re: [isabelle] operator on predicates and relations
On 03/04/14 09:31, Viorel Preoteasa wrote:
The overloading target is documented in the isar-ref manual in section 5.8. It also works
If you want to use more advanced definition facilities
(definition/function/...), you should have a look at "context
overloading ... begin" context blocks.
Where can I find more information and examples about this mechanism?
There are a number of examples usages in the HOL sources, e.g., in ~~/src/HOL/Nat and
~~/src/HOL/Algebra/Groups. Here's another example:
myop_A == "myop :: 'a A"
definition myop_A :: "'a A" where "myop_A P = P"
This archive was generated by a fusion of
Pipermail (Mailman edition) and