changeset 10877 | 6417de2029b0 |
parent 10846 | 623141a08705 |
child 10958 | fd582f0d649b |
--- a/doc-src/TutorialI/Rules/Forward.thy Fri Jan 12 11:08:06 2001 +0100 +++ b/doc-src/TutorialI/Rules/Forward.thy Fri Jan 12 16:05:12 2001 +0100 @@ -144,6 +144,11 @@ lemma relprime_20_81: "gcd(#20,#81) = 1"; by (simp add: gcd.simps) +text{*example of arg_cong (NEW) + +@{thm[display] arg_cong[no_vars]} +\rulename{arg_cong} +*} text {*