(* Title: WordInterval.thy Authors: Julius Michaelis, Cornelius Diekmann *) theory WordInterval imports Main "Word_Lib.Word_Lemmas" "Word_Lib.Next_and_Prev" begin section‹WordInterval: Executable datatype for Machine Word Sets› text‹Stores ranges of machine words as interval. This has been proven quite efficient for IP Addresses.› (*NOTE: All algorithms here use a straight-forward implementation. There is a lot of room for improving the computation complexity, for example by making the WordInterval a balanced, sorted tree.*) subsection‹Syntax› context notes [[typedef_overloaded]] begin