src/Pure/variable.ML
changeset 24867 e5b55d7be9bb
parent 24848 5dbbd33c3236
child 25051 71cd45fdf332
equal deleted inserted replaced
24866:6e6d9e80ebb4 24867:e5b55d7be9bb