src/HOL/Auth/Message.thy
changeset 21404 eb85850d3eb7
parent 20648 742c30fc3fcb
child 21588 cd0dc678a205