Theory Examples2

theory Examples2
imports Examples
begin
  interpretation %visible int: partial_order "(≤) :: [int, int] ⇒ bool"
    rewrites "int.less x y = (x < y)"
  proof -
    txt ‹\normalsize The goals are now:
      @{subgoals [display]}
      The proof that~‹≤› is a partial order is as above.›
    show "partial_order ((≤) :: int ⇒ int ⇒ bool)"
      by unfold_locales auto
    txt ‹\normalsize The second goal is shown by unfolding the
      definition of \<^term>‹partial_order.less›.›
    show "partial_order.less (≤) x y = (x < y)"
      unfolding partial_order.less_def [OF ‹partial_order (≤)›]
      by auto
  qed

text ‹Note that the above proof is not in the context of the
  interpreted locale.  Hence, the premise of ‹partial_order.less_def› is discharged manually with ‹OF›.
›
end