src/HOL/Tools/function_package/auto_term.ML
changeset 21258 62f25a96f0c1
parent 21104 b6ab939147eb
child 21319 cf814e36f788
equal deleted inserted replaced
21257:b7f090c5057d 21258:62f25a96f0c1