src/HOL/Nominal/nominal_induct.ML
changeset 20205 7b2958d3d575
parent 20072 c4710df2c953
child 20288 8ff4a0ea49b2
equal deleted inserted replaced
20204:2842450d0eee 20205:7b2958d3d575