src/HOL/Auth/Guard/Extensions.thy
changeset 17111 d2ea9c974570
parent 16417 9bc16273c2d4
child 17689 a04b5b43625e
equal deleted inserted replaced
17110:4c5622d7bdbe 17111:d2ea9c974570