src/Pure/General/exn.ML
changeset 41648 6d736d983d5c
parent 40483 3848283c14bb
child 42223 098c86e53153
equal deleted inserted replaced
41647:5e70526a1947 41648:6d736d983d5c