src/HOL/Fun_Def.thy
changeset 55430 8eb6c740ec1a
parent 55085 0e8e4dc55866
child 55466 786edc984c98
equal deleted inserted replaced
55429:4a50f9e70dc1 55430:8eb6c740ec1a