src/HOL/Auth/Recur.thy
changeset 31106 9a1178204dc0
parent 24122 fc7f857d33c8
child 32404 da3ca3c6ec81