src/HOL/Tools/inductive_realizer.ML
changeset 31213 800787c3210f
parent 31177 c39994cb152a
child 31458 b1cf26f2919b