DEFABBREV DEFABBREV : making a macro look like a function In the theorem prover Controlled expansion of definition Usable on left side of rewrite rule In the simulator Performance improvement through inlined code Encapsulate compiler declarations Possible STOBJ transparency (?)