src/HOL/Tools/inductive_realizer.ML
changeset 59209 8521841f277b
parent 59058 a78612c67ec0
child 59498 50b60f501b05