| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Java/Openjdk/src/hotspot/share/gc/z/ (Sun/Oracle ©) Datei vom 13.11.2022 mit Größe 3 kB |
|
SSL Packet.thyInteraktion undPortierbarkeitIsabelle |
|||||||||||||||
|
(* Title: HOL/HOLCF/IOA/NTP/Packet.thy Author: Tobias Nipkow & Konrad Slind *) theory Packet imports Multiset begin type_synonym 'msg packet = "bool * 'msg" definition hdr :: "'msg packet ==> bool" where "hdr ≡ fst" definition msg :: "'msg packet ==> 'msg" where "msg ≡ snd" text ‹Instantiation of a tautology?› lemma eq_packet_imp_eq_hdr: "∀x. x = packet ⟶ hdr(x) = hdr(packet)" by simp declare hdr_def [simp] msg_def [simp] end
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.11Angebot (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-05-01) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26