src/HOL/Tools/Lifting/lifting_def.ML
changeset 79514 9204c034a5bf
parent 78095 bc42c074e58f
child 80673 5aa376b7abb8
equal deleted inserted replaced
79513:292605271dcf 79514:9204c034a5bf