| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Word_Lib/ (Archive of formal Proofs Version 2026-5©) Datei vom 29.4.2026 mit Größe 481 B |
|
Quelle Word_16.thy Sprache: Isabelle |
|||||||||||||||||||||||||
|
(* * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) section "Words of Length 16" theory Word_16 imports More_Word Signed_Words begin lemma len16: "len_of (x :: 16 itself) = 16" by simp context includes bit_operations_syntax begin lemma word16_and_max_simp: ‹x AND 0xFFFF = x› for x :: ‹16 word› using word_and_full_mask_simp [of x] by (simp add: numeral_eq_Suc mask_Suc_exp) end end
¤ Dauer der Verarbeitung: 0.1 Sekunden ¤*© Formatika GbR, Deutschland |
|
||||||||||||||||||||||||
2026-11-01