src/HOL/Auth/Recur.ML
changeset 6675 63e53327f5e5
parent 5535 678999604ee9
child 7057 b9ddbb925939
equal deleted inserted replaced
6674:32892a8ecb15 6675:63e53327f5e5