src/HOL/Nominal/nominal_inductive.ML
changeset 57987 ecb227b40907
parent 57884 36b5691b81a5
child 58112 8081087096ad
equal deleted inserted replaced
57986:0d60b9e58487 57987:ecb227b40907