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
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet am 2026-06-30)
¤
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 und die Messung sind noch experimentell.
