# HG changeset patch
# User paulson
# Date 994852848 -7200
# Node ID 138919f1a135af5381fa4018764e122996fe5ccf
# Parent  2b17622e1929b9d6b32dc725303a890c17156bf9
tweaks for new version

diff -r 2b17622e1929 -r 138919f1a135 doc-src/TutorialI/Rules/Basic.thy
--- a/doc-src/TutorialI/Rules/Basic.thy	Wed Jul 11 13:57:01 2001 +0200
+++ b/doc-src/TutorialI/Rules/Basic.thy	Wed Jul 11 14:00:48 2001 +0200
@@ -136,6 +136,9 @@
 @{thm[display] contrapos_pp}
 \rulename{contrapos_pp}
 
+@{thm[display] contrapos_pn}
+\rulename{contrapos_pn}
+
 @{thm[display] contrapos_np}
 \rulename{contrapos_np}
 
@@ -263,7 +266,9 @@
 	--{* @{subgoals[display,indent=0,margin=65]} *}
 apply (erule exE) 
 	--{* @{subgoals[display,indent=0,margin=65]} *}
-apply (rule_tac x="k*ka" in exI) 
+apply (rename_tac l)
+	--{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule_tac x="k*l" in exI) 
 	--{* @{subgoals[display,indent=0,margin=65]} *}
 apply simp
 done
@@ -394,7 +399,7 @@
  apply assumption
 oops
 
-lemma "\<forall> y. R y y \<Longrightarrow> \<exists>x. \<forall> y. R x y"
+lemma "\<forall>y. R y y \<Longrightarrow> \<exists>x. \<forall>y. R x y"
 apply (rule exI) 
   --{* @{subgoals[display,indent=0,margin=65]} *}
 apply (rule allI) 
@@ -403,13 +408,13 @@
   --{* @{subgoals[display,indent=0,margin=65]} *}
 oops
 
-lemma "\<forall>x. \<exists> y. x=y"
+lemma "\<forall>x. \<exists>y. x=y"
 apply (rule allI)
 apply (rule exI)
 apply (rule refl)
 done
 
-lemma "\<exists>x. \<forall> y. x=y"
+lemma "\<exists>x. \<forall>y. x=y"
 apply (rule exI)
 apply (rule allI)
 oops
diff -r 2b17622e1929 -r 138919f1a135 doc-src/TutorialI/Rules/Force.thy
--- a/doc-src/TutorialI/Rules/Force.thy	Wed Jul 11 13:57:01 2001 +0200
+++ b/doc-src/TutorialI/Rules/Force.thy	Wed Jul 11 14:00:48 2001 +0200
@@ -1,6 +1,14 @@
 (* ID:         $Id$ *)
-theory Force = Main:
+theory Force = Divides: (*Divides rather than Main so that the first proof
+                         isn't done by the nat_divide_cancel_factor simprocs.*)
+
+declare div_mult_self_is_m [simp del];
 
+lemma div_mult_self_is_m: 
+      "0<n \<Longrightarrow> (m*n) div n = (m::nat)"
+apply (insert mod_div_equality [of "m*n" n])
+apply simp
+done
 
 
 lemma "(\<forall>x. P x) \<and> (\<exists>x. Q x) \<longrightarrow> (\<forall>x. P x \<and> Q x)"
diff -r 2b17622e1929 -r 138919f1a135 doc-src/TutorialI/Rules/Forward.thy
--- a/doc-src/TutorialI/Rules/Forward.thy	Wed Jul 11 13:57:01 2001 +0200
+++ b/doc-src/TutorialI/Rules/Forward.thy	Wed Jul 11 14:00:48 2001 +0200
@@ -154,7 +154,7 @@
 *}
 
 lemma relprime_dvd_mult: 
-      "\<lbrakk> gcd(k,n)=1; k dvd m*n \<rbrakk> \<Longrightarrow> k dvd m";
+      "\<lbrakk> gcd(k,n)=1; k dvd m*n \<rbrakk> \<Longrightarrow> k dvd m"
 apply (insert gcd_mult_distrib2 [of m k n])
 apply simp
 apply (erule_tac t="m" in ssubst);
@@ -169,11 +169,9 @@
 \rulename{mod_div_equality}
 *};
 
-lemma div_mult_self_is_m: 
-      "0<n \<Longrightarrow> (m*n) div n = (m::nat)"
-apply (insert mod_div_equality [of "m*n" n])
-apply simp
-done
+(*MOVED to Force.thy, which now depends only on Divides.thy
+lemma div_mult_self_is_m: "0<n \<Longrightarrow> (m*n) div n = (m::nat)"
+*)
 
 lemma relprime_dvd_mult_iff: "gcd(k,n)=1 \<Longrightarrow> (k dvd m*n) = (k dvd m)";
 by (blast intro: relprime_dvd_mult dvd_trans)
diff -r 2b17622e1929 -r 138919f1a135 doc-src/TutorialI/Rules/Tacticals.thy
--- a/doc-src/TutorialI/Rules/Tacticals.thy	Wed Jul 11 13:57:01 2001 +0200
+++ b/doc-src/TutorialI/Rules/Tacticals.thy	Wed Jul 11 14:00:48 2001 +0200
@@ -34,7 +34,6 @@
 
 lemma "bigsubgoal1 \<and> bigsubgoal2 \<and> bigsubgoal3 \<and> bigsubgoal4 \<and> bigsubgoal5 \<and> bigsubgoal6"
 apply intro   --{* @{subgoals[display,indent=0,margin=65]} *}
-pr 2  
 txt{* @{subgoals[display,indent=0,margin=65]} 
 A total of 6 subgoals...
 *}