# HG changeset patch
# User paulson
# Date 971772351 -7200
# Node ID 20cf817f3b4ad6effcda7d6117cd1407f6d6a47f
# Parent  c8726d4ee89a64e2717eb78f0e66855946507414
renaming of contrapos rules

diff -r c8726d4ee89a -r 20cf817f3b4a doc-src/TutorialI/CTL/CTL.thy
--- a/doc-src/TutorialI/CTL/CTL.thy	Tue Oct 17 10:27:28 2000 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy	Tue Oct 17 10:45:51 2000 +0200
@@ -175,14 +175,14 @@
 
 lemma not_in_lfp_afD:
  "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t)\<in>M \<and> t \<notin> lfp(af A))";
-apply(erule swap);
+apply(erule contrapos_np);
 apply(rule ssubst[OF lfp_unfold[OF mono_af]]);
 apply(simp add:af_def);
 done;
 
 text{*\noindent
-is proved by a variant of contraposition (@{thm[source]swap}:
-@{thm swap[no_vars]}), i.e.\ assuming the negation of the conclusion
+is proved by a variant of contraposition (@{thm[source]contrapos_np}:
+@{thm contrapos_np[no_vars]}), i.e.\ assuming the negation of the conclusion
 and proving @{term"s : lfp(af A)"}. Unfolding @{term lfp} once and
 simplifying with the definition of @{term af} finishes the proof.
 
@@ -333,12 +333,12 @@
 "{s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
 
 txt{*\noindent
-The proof is again pointwise and then by contraposition (@{thm[source]contrapos2} is the rule
-@{thm contrapos2}):
+The proof is again pointwise and then by contraposition (@{thm[source]contrapos_pp} is the rule
+@{thm contrapos_pp}):
 *};
 
 apply(rule subsetI);
-apply(erule contrapos2);
+apply(erule contrapos_pp);
 apply simp;
 (*pr(latex xsymbols symbols);*)
 
diff -r c8726d4ee89a -r 20cf817f3b4a doc-src/TutorialI/CTL/CTLind.thy
--- a/doc-src/TutorialI/CTL/CTLind.thy	Tue Oct 17 10:27:28 2000 +0200
+++ b/doc-src/TutorialI/CTL/CTLind.thy	Tue Oct 17 10:45:51 2000 +0200
@@ -110,7 +110,7 @@
 the contraposition.
 *}
 
-apply(erule contrapos2);
+apply(erule contrapos_pp);
 apply(simp add:wf_iff_no_infinite_down_chain);
 apply(erule exE);
 apply(rule ex_infinite_path);