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