* Isar: command 'declaration'; * Isar: proper interfaces for simplification procedures; * Isar: an extra pair of brackets around attribute declarations abbreviates a theorem reference involving an internal dummy fact;