src/HOL/BCV/Err.ML
changeset 10527 7934b0fa8dcc
parent 10172 3daeda3d3cd0
child 11224 5f10ca5e0b49
equal deleted inserted replaced
10526:ced4f4ec917e 10527:7934b0fa8dcc