| products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 57 kB |
|
SSL Case_Product.thyInteraktion undPortierbarkeitIsabelle |
|||||||||||||||
|
(* 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
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.10Angebot (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-29) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26