src/Pure/unify.ML
changeset 910 822e57491612
parent 651 4b0455fbcc49
child 922 196ca0973a6d