equal
deleted
inserted
replaced
385 \<close> |
385 \<close> |
386 |
386 |
387 lemma "0 + (x + 0) = x + 0 + 0" apply simp? oops |
387 lemma "0 + (x + 0) = x + 0 + 0" apply simp? oops |
388 |
388 |
389 text \<open> |
389 text \<open> |
390 The above attempt \<^emph>\<open>fails\<close>, because @{term "0"} and @{term "op +"} in the |
390 The above attempt \<^emph>\<open>fails\<close>, because @{term "0"} and @{term "(+)"} in the |
391 HOL library are declared as generic type class operations, without stating |
391 HOL library are declared as generic type class operations, without stating |
392 any algebraic laws yet. More specific types are required to get access to |
392 any algebraic laws yet. More specific types are required to get access to |
393 certain standard simplifications of the theory context, e.g.\ like this:\<close> |
393 certain standard simplifications of the theory context, e.g.\ like this:\<close> |
394 |
394 |
395 lemma fixes x :: nat shows "0 + (x + 0) = x + 0 + 0" by simp |
395 lemma fixes x :: nat shows "0 + (x + 0) = x + 0 + 0" by simp |