| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Doc/Locales/ (Isabelle Prover Version 2025-1©) Datei vom 16.11.2025 mit Größe 944 B |
|
Quelle Examples2.thySprache: Isabelle |
|||||||||||||||
|
theory Examples2 imports Examples begin 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 ‹ ›
¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet am 2026-08-25) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-08-25