src/HOL/Auth/Recur.thy
changeset 4447 b7ee449eb345
parent 3683 aafe719dff14
child 4552 bb8ff763c93d