src/HOL/Tools/inductive_realizer.ML
changeset 31276 f6427bc40421
parent 31177 c39994cb152a
child 31458 b1cf26f2919b