src/HOL/NatDef.ML
changeset 11276 f8353c722d4e
parent 11135 8fd0dea26286
child 11326 680ebd093cfe
equal deleted inserted replaced
11275:71498de45241 11276:f8353c722d4e