src/HOL/Auth/Message.thy
changeset 2045 ae1030e66745
parent 2032 1bbf1bdcaf56
child 2121 7e118eb32bdc