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