src/Pure/pattern.ML
changeset 13097 c9c7f23d0ceb
parent 12980 8f717cbd4e44
child 13195 98975cc13d28
equal deleted inserted replaced
13096:04f8cbd1b500 13097:c9c7f23d0ceb