src/HOL/Auth/Recur.ML
changeset 3512 9dcb4daa15e8
parent 3483 6988394a6008
child 3516 470626799511
equal deleted inserted replaced
3511:da4dd8b7ced4 3512:9dcb4daa15e8