src/HOL/Auth/Recur.thy
changeset 24967 68c5c62bed13
parent 24122 fc7f857d33c8
child 32404 da3ca3c6ec81