src/HOL/Tools/inductive_realizer.ML
changeset 21225 bf0b1e62cf60
parent 21022 3634641f9405
child 21395 f34ac19659ae