src/HOL/Word/Traditional_Syntax.thy
changeset 72050 d4de7e4754d2
parent 72000 379d0c207c29
child 72508 c89d8e8bd8c7