changeset 10877 | 6417de2029b0 |
parent 10846 | 623141a08705 |
child 10958 | fd582f0d649b |
10876:e12892e4666a | 10877:6417de2029b0 |
---|---|
142 |
142 |
143 |
143 |
144 lemma relprime_20_81: "gcd(#20,#81) = 1"; |
144 lemma relprime_20_81: "gcd(#20,#81) = 1"; |
145 by (simp add: gcd.simps) |
145 by (simp add: gcd.simps) |
146 |
146 |
147 text{*example of arg_cong (NEW) |
|
148 |
|
149 @{thm[display] arg_cong[no_vars]} |
|
150 \rulename{arg_cong} |
|
151 *} |
|
147 |
152 |
148 |
153 |
149 text {* |
154 text {* |
150 Examples of 'OF' |
155 Examples of 'OF' |
151 |
156 |