src/HOL/Auth/Guard/P1.thy
changeset 79587 f9038dd937dd
parent 76288 b82ac7ef65ec