Example. Simplifier rules for nand [isa-001I]

Continuing our nand example, we can prove theorems and attach the [simp] attribute simultaneously: lemma nand_t[simp]: ‹nand True A = (¬ A)› apply (unfold nand_def) apply simp done Alternatively, we can add theorems after-the-fact like so: lemma nand_f: ‹nand False A = True› apply (unfold nand_def) apply simp done (* ... *) declare nand_f[simp] Occasionally it becomes useful to remove a theorem from the simp set. This can be achieved by using the declare command and the [simp del] attribute:

declare nand_f[simp del]