src/HOL/Tools/inductive_realizer.ML
changeset 31941 d3a94ae9936f
parent 31784 bd3486c57ba3
child 31986 a68f88d264f7