# HG changeset patch # User paulson # Date 979311912 -3600 # Node ID 6417de2029b089dfb98bf8230d1bcd6952356e43 # Parent e12892e4666a4e02bdab24b3194aa5f4bf7bc126 general revisions diff -r e12892e4666a -r 6417de2029b0 doc-src/TutorialI/Rules/Forward.thy --- 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 {*