src/HOL/Nominal/nominal_inductive2.ML
changeset 61569 947ce60a06e1
parent 61144 5e94dfead1c2
child 62913 13252110a6fe
equal deleted inserted replaced
61568:26c76e143b77 61569:947ce60a06e1