src/HOL/Auth/Recur.thy
changeset 7405 7e4e286a9931
parent 5434 9b4bed3f394c
child 11185 1b737b4c2108
equal deleted inserted replaced
7404:e488cf3da60a 7405:7e4e286a9931