src/HOL/Tools/inductive_realizer.ML
changeset 31106 9a1178204dc0
parent 30722 623d4831c8cf
child 31174 f1f1e9b53c81