src/Pure/pattern.ML
changeset 12902 a23dc0b7566f
parent 12826 dfb214fa310b
child 12980 8f717cbd4e44
equal deleted inserted replaced
12901:4570584fbda9 12902:a23dc0b7566f