src/Pure/more_pattern.ML
changeset 78344 4aa3d3aa57b3
parent 74525 c960bfcb91db
child 79242 b0774e7d1949
equal deleted inserted replaced
78343:1932737e55a9 78344:4aa3d3aa57b3