| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/ex/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 689 B |
|
Quelle Case_Product.thySprache: Isabelle |
|||||||||||||||
|
(* Title: HOL/ex/Case_Product.thy Author: Lars Noschinski Copyright 2011 TU Muenchen *) section ‹Examples for the 'case_product' attribute› theory Case_Product imports Main begin text ‹ The @{attribute case_product} attribute combines multiple case distinction lemmas into a single case distinction lemma by building the product of all these case distinctions. › lemmas nat_list_exhaust = nat.exhaust [case_product list.exhaust] text ‹The attribute honours preconditions.› lemmas trancl_acc_cases = trancl.cases [case_product acc.cases] text ‹Also, case names are generated based on the old names.› end
¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet am 2026-06-09) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09