src/HOL/Tools/inductive_realizer.ML
changeset 15872 8336ff711d80
parent 15706 bc264e730103
child 16123 1381e90c2694