src/HOL/Word/TdThs.thy
changeset 30273 ecd6f0ca62ea
parent 29631 3aa049e5f156
child 30729 461ee3e49ad3