# HG changeset patch
# User paulson
# Date 979127020 -3600
# Node ID 2c64c7991f7cd1cc23465b62bd09519aabed5532
# Parent  49868b703e4d3e2f3b36e5adb5131f826af4b891
case_tac subgoals

diff -r 49868b703e4d -r 2c64c7991f7c doc-src/TutorialI/Rules/Primes.thy
--- a/doc-src/TutorialI/Rules/Primes.thy	Wed Jan 10 11:16:38 2001 +0100
+++ b/doc-src/TutorialI/Rules/Primes.thy	Wed Jan 10 12:43:40 2001 +0100
@@ -81,9 +81,18 @@
       "k dvd m \<longrightarrow> k dvd n \<longrightarrow> k dvd gcd(m,n)"
 apply (induct_tac m n rule: gcd.induct)
 apply (case_tac "n=0")
+txt{*subgoals after the case tac
+@{subgoals[display,indent=0,margin=65]}
+*};
 apply (simp_all add: dvd_mod)
 done
 
+(*just checking the claim that case_tac "n" works too*)
+lemma "k dvd m \<longrightarrow> k dvd n \<longrightarrow> k dvd gcd(m,n)"
+apply (induct_tac m n rule: gcd.induct)
+apply (case_tac "n")
+by (simp_all add: dvd_mod)
+
 theorem gcd_greatest_iff [iff]: 
         "(k dvd gcd(m,n)) = (k dvd m \<and> k dvd n)"
 by (blast intro!: gcd_greatest intro: dvd_trans)