src/Pure/General/symbol_pos.ML
changeset 43444 f744902b4681
parent 42503 27514b6fbe93
child 43709 717e96cf9527