src/HOL/Auth/Recur.thy
changeset 29667 53103fc8ffa3
parent 24122 fc7f857d33c8
child 32404 da3ca3c6ec81