src/HOL/Tools/inductive_realizer.ML
changeset 70345 80a1aa30e24d
parent 69829 3bfa28b3a5b2
child 70412 64ead6de6212