Nominal-General/nominal_library.ML
changeset 2195 0c1dcdefb515
parent 1979 760257a66604
child 2288 3b83960f9544
equal deleted inserted replaced
2194:a52499e125ce 2195:0c1dcdefb515