src/HOL/Tools/inductive_realizer.ML
changeset 29380 a9ee3475abf4
parent 29281 b22ccb3998db
child 29389 0a49f940d729