src/HOL/Tools/inductive_realizer.ML
changeset 31101 26c7bb764a38
parent 30722 623d4831c8cf
child 31174 f1f1e9b53c81