src/HOL/Nominal/nominal_induct.ML
changeset 29805 a5da150bd0ab
parent 29581 b3b33e0298eb
child 30092 9c3b1c136d1f
equal deleted inserted replaced
29804:e15b74577368 29805:a5da150bd0ab