src/HOL/Tools/inductive_realizer.ML
changeset 19759 2d0896653e7a
parent 19617 7cb4b67d4b97
child 19806 f860b7a98445