case_tac subgoals
Wed, 10 Jan 2001 12:43:40 +0100
changeset 10853 2c64c7991f7c
parent 10852 49868b703e4d
child 10854 d1ff1ff5c5ad
case_tac subgoals
--- 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
 apply (simp_all add: dvd_mod)
+(*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)