src/HOL/Tools/inductive_realizer.ML
changeset 29401 94fd5dd918f5
parent 29281 b22ccb3998db
child 29389 0a49f940d729