src/Tools/interpretation_with_defs.ML
changeset 42338 802f2fe7a0c9
parent 41582 c34415351b6d
child 42361 23f352990944
equal deleted inserted replaced
42337:fef417b12f38 42338:802f2fe7a0c9