src/HOL/Nominal/nominal_inductive2.ML
changeset 29805 a5da150bd0ab
parent 29585 c23295521af5
child 30087 a780642a9c9c
child 30240 5b25fee0362c
equal deleted inserted replaced
29804:e15b74577368 29805:a5da150bd0ab