src/Pure/Syntax/xgram.ML
changeset 13244 7b37e218f298
parent 18 c9ec452ff08f
equal deleted inserted replaced
13243:ba53d07d32d5 13244:7b37e218f298