1.1 --- a/doc-src/TutorialI/Rules/Primes.thy	Wed Jan 10 11:16:38 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Rules/Primes.thy	Wed Jan 10 12:43:40 2001 +0100
     1.3 @@ -81,9 +81,18 @@
     1.4        "k dvd m \<longrightarrow> k dvd n \<longrightarrow> k dvd gcd(m,n)"
     1.5  apply (induct_tac m n rule: gcd.induct)
     1.6  apply (case_tac "n=0")
     1.7 +txt{*subgoals after the case tac
     1.8 +@{subgoals[display,indent=0,margin=65]}
     1.9 +*};
    1.10  apply (simp_all add: dvd_mod)
    1.11  done
    1.12  
    1.13 +(*just checking the claim that case_tac "n" works too*)
    1.14 +lemma "k dvd m \<longrightarrow> k dvd n \<longrightarrow> k dvd gcd(m,n)"
    1.15 +apply (induct_tac m n rule: gcd.induct)
    1.16 +apply (case_tac "n")
    1.17 +by (simp_all add: dvd_mod)
    1.18 +
    1.19  theorem gcd_greatest_iff [iff]: 
    1.20          "(k dvd gcd(m,n)) = (k dvd m \<and> k dvd n)"
    1.21  by (blast intro!: gcd_greatest intro: dvd_trans)