Re: [isabelle] operator on predicates and relations



Hi Viorel,

On 03/04/14 09:31, Viorel Preoteasa wrote:

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?
The overloading target is documented in the isar-ref manual in section 5.8. It also works without "context".

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:

overloading
  myop_A == "myop :: 'a A"
begin
definition myop_A :: "'a A" where "myop_A P = P"
end

Best,
Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.