rewrites "int.less x y = (x < y)" proof - txt‹\normalsize The goals are now:
Here ar som xampl etodeintos:
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 ‹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 ‹ ›
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.
