| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/FOL/ex/Locale_Test/ (Isabelle Prover Version 2025-1©) Datei vom 16.11.2025 mit Größe 658 B |
|
Quelle Locale_Test2.thySprache: Isabelle |
|||||||||||||||
|
(* Title: FOL/ex/Locale_Test/Locale_Test2.thy Author: Clemens Ballarin, TU Muenchen Test environment for the locale implementation. *) theory Locale_Test2 imports Locale_Test1 begin interpretation le1: mixin_thy_merge ‹gle› ‹gle'› rewrites ‹reflexive.less(gle, x, y) ⟷ gless(x, y)› proof - show ‹mixin_thy_merge(gle, gle')› by unfold_locales note reflexive = this[unfolded mixin_thy_merge_def, THEN conjunct1] show ‹reflexive.less(gle, x, y) ⟷ gless(x, y)› by (simp add: reflexive.less_def[OF reflexive] gless_def) qed end
¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet am 2026-06-29) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09