src/HOL/Auth/Event.ML
changeset 4246 c539e702e1d2
parent 4091 771b1f6422a8
child 4266 dab1833cb26d
equal deleted inserted replaced
4245:b9ce25073cc0 4246:c539e702e1d2