src/Pure/Syntax/syn_ext.ML
changeset 2495 82ec47e0a8d3
parent 2382 e7c2bce815ba
child 2694 b98365c6e869
equal deleted inserted replaced
2494:5d45c2094ff6 2495:82ec47e0a8d3