--- a/doc-src/TutorialI/Rules/Forward.thy Fri Nov 02 15:56:49 2007 +0100
+++ b/doc-src/TutorialI/Rules/Forward.thy Fri Nov 02 16:38:14 2007 +0100
@@ -102,6 +102,14 @@
text {*
+@{thm[display] gcd_mult}
+\rulename{gcd_mult}
+
+@{thm[display] gcd_self0}
+\rulename{gcd_self0}
+*};
+
+text {*
Rules handy with THEN
@{thm[display] iffD1}
@@ -161,13 +169,18 @@
lemma relprime_dvd_mult:
"\<lbrakk> gcd k n = 1; k dvd m*n \<rbrakk> \<Longrightarrow> k dvd m"
apply (insert gcd_mult_distrib2 [of m k n])
+txt{*@{subgoals[display,indent=0,margin=65]}*}
apply simp
+txt{*@{subgoals[display,indent=0,margin=65]}*}
apply (erule_tac t="m" in ssubst);
apply simp
done
text {*
+@{thm[display] relprime_dvd_mult}
+\rulename{relprime_dvd_mult}
+
Another example of "insert"
@{thm[display] mod_div_equality}