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 🍋‹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-04-27)
¤
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.
