src/HOL/Tools/inductive_realizer.ML
changeset 59523 860fb1c65553
parent 59498 50b60f501b05
child 59582 0fbed69ff081