src/HOL/Tools/inductive_realizer.ML
changeset 31489 10080e31b294
parent 31458 b1cf26f2919b
child 31668 a616e56a5ec8