src/HOL/Nominal/nominal_inductive.ML
changeset 29457 2eadbc24de8c
parent 29287 5b0bfd63b5da
child 29585 c23295521af5
equal deleted inserted replaced
29456:3f8b85444512 29457:2eadbc24de8c