src/HOL/Import/HOL/prim_rec.imp
changeset 15635 8408a06590a6
parent 14516 a183dec876ab
child 19277 f7602e74d948