1theory Examples2
2imports Examples
3begin
4  interpretation %visible int: partial_order "(\<le>) :: [int, int] \<Rightarrow> bool"
5    rewrites "int.less x y = (x < y)"
6  proof -
7    txt \<open>\normalsize The goals are now:
8      @{subgoals [display]}
9      The proof that~@{text \<le>} is a partial order is as above.\<close>
10    show "partial_order ((\<le>) :: int \<Rightarrow> int \<Rightarrow> bool)"
11      by unfold_locales auto
12    txt \<open>\normalsize The second goal is shown by unfolding the
13      definition of @{term "partial_order.less"}.\<close>
14    show "partial_order.less (\<le>) x y = (x < y)"
15      unfolding partial_order.less_def [OF \<open>partial_order (\<le>)\<close>]
16      by auto
17  qed
18
19text \<open>Note that the above proof is not in the context of the
20  interpreted locale.  Hence, the premise of @{text
21  "partial_order.less_def"} is discharged manually with @{text OF}.
22\<close>
23end
24