src/HOL/BCV/Types.thy
changeset 9450 c97dba47e504
parent 7626 5997f35954d7