src/Pure/sorts.ML
changeset 75616 986506233812
parent 74234 4f2bd13edce3
child 77730 4a174bea55e2
equal deleted inserted replaced
75615:4494cd69f97f 75616:986506233812