Nominal/nominal_basics.ML
changeset 3221 ea327a4c4f43
parent 3214 13ab4f0a0b0e
child 3229 b52e8651591f
equal deleted inserted replaced
3220:87dbeba4b25a 3221:ea327a4c4f43