| changeset 61798 | 27f3c10b0b50 |
| parent 60770 | 240563fbf41d |
| child 63648 | f9f3006a5579 |
--- a/src/ZF/ArithSimp.thy Mon Dec 07 10:19:30 2015 +0100 +++ b/src/ZF/ArithSimp.thy Mon Dec 07 10:23:50 2015 +0100 @@ -264,7 +264,7 @@ by (cut_tac n = 0 in mod2_add_more, auto) -subsection\<open>Additional theorems about @{text "\<le>"}\<close> +subsection\<open>Additional theorems about \<open>\<le>\<close>\<close> lemma add_le_self: "m:nat ==> m \<le> (m #+ n)" apply (simp (no_asm_simp))