theory Examples2 imports Examples begin interpretation %visible int: partial_order "(\) :: [int, int] \ bool"
rewrites "int.less x y = (x < y)" proof - txt\<open>\normalsize The goals are now:
@{subgoals [display]}
The proof that~\<open>\<le>\<close> is a partial order is as above.\<close> show"partial_order ((\) :: int \ int \ bool)" by unfold_locales auto txt\<open>\normalsize The second goal is shown by unfolding the definition of \<^term>\<open>partial_order.less\<close>.\<close> show"partial_order.less (\) x y = (x < y)" unfolding partial_order.less_def [OF \<open>partial_order (\<le>)\<close>] by auto qed
text\<open>Note that the above proof is not in the context of the
interpreted locale. Hence, the premise of \<open>partial_order.less_def\<close> is discharged manually with \<open>OF\<close>. \<close> end
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
