src/HOL/Auth/Event.thy
changeset 73934 39e0c7fac69e
parent 69597 ff784d5a5bfb
child 76287 cdc14f94c754
equal deleted inserted replaced
73933:fa92bc604c59 73934:39e0c7fac69e