src/HOL/Fun.thy
changeset 30430 42ea5d85edcc
parent 30301 429612400fe9
child 31080 21ffc770ebc0
equal deleted inserted replaced
30429:39acdf031548 30430:42ea5d85edcc