src/HOL/SET_Protocol/Purchase.thy
changeset 78660 0d2ea608d223
parent 69597 ff784d5a5bfb