src/Pure/General/exn.ML
changeset 80161 fd5ed5e63a29
parent 78764 a3dcae9a2ebe
equal deleted inserted replaced
80160:ead20482da9c 80161:fd5ed5e63a29