src/HOL/Tools/Function/function_common.ML
changeset 66828 3c936ebebc23
parent 65387 5dbe02addca5
child 67149 e61557884799
equal deleted inserted replaced
66825:9f6ec65f7a6e 66828:3c936ebebc23