src/HOL/Tools/inductive_realizer.ML
changeset 70901 94a0c47b8553
parent 70840 5b80eb4fd0f3
child 70915 bd4d37edfee4