src/HOL/Tools/inductive_realizer.ML
changeset 29401 94fd5dd918f5
parent 29281 b22ccb3998db
child 29389 0a49f940d729
equal deleted inserted replaced
29374:ff4ba1ed4527 29401:94fd5dd918f5