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