src/HOL/UNITY/GenPrefix.ML
changeset 7539 680eca63b98e
parent 7499 23e090051cb8
child 7839 03fd460cb8b8