src/Pure/pure_syn.ML
changeset 49681 aa66ea552357
parent 48905 04576657cf94
child 52455 9a8f4fdac3cf
equal deleted inserted replaced
49680:00290dc6bfad 49681:aa66ea552357