src/Pure/more_pattern.ML
changeset 82282 919eb0e67930
parent 81253 bbed9f218158
equal deleted inserted replaced
82281:9357ef19fc56 82282:919eb0e67930