src/HOL/Tools/Function/function.ML
changeset 82470 785615e37846
parent 81466 bb82ebb18b5d
child 82967 73af47bc277c
equal deleted inserted replaced
82469:1fa80133027d 82470:785615e37846