equal
deleted
inserted
replaced
1073 lemmas nat_1_add_1 = one_add_one [where 'a=nat] (* legacy *) |
1073 lemmas nat_1_add_1 = one_add_one [where 'a=nat] (* legacy *) |
1074 |
1074 |
1075 |
1075 |
1076 subsection {* Particular lemmas concerning @{term 2} *} |
1076 subsection {* Particular lemmas concerning @{term 2} *} |
1077 |
1077 |
1078 context linordered_field_inverse_zero |
1078 context linordered_field |
1079 begin |
1079 begin |
1080 |
1080 |
1081 lemma half_gt_zero_iff: |
1081 lemma half_gt_zero_iff: |
1082 "0 < a / 2 \<longleftrightarrow> 0 < a" (is "?P \<longleftrightarrow> ?Q") |
1082 "0 < a / 2 \<longleftrightarrow> 0 < a" (is "?P \<longleftrightarrow> ?Q") |
1083 by (auto simp add: field_simps) |
1083 by (auto simp add: field_simps) |