src/HOL/Tools/inductive_realizer.ML
changeset 17970 a84ac7c201ea
parent 17959 8db36a108213
child 18008 f193815cab2c