src/Pure/display.ML
changeset 4962 e9217cb15b42
parent 4950 226f2cde9f4d
child 4993 2055bfbb186c