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 {*