src/HOL/Auth/Recur.thy
changeset 13710 75bec2c1bfd5
parent 13507 febb8e5d2a9d
child 13922 75ae4244a596