src/HOL/Import/HOL/one.imp
changeset 40786 0a54cfc9add3
parent 14516 a183dec876ab