# HG changeset patch
# User wenzelm
# Date 1134069357 -3600
# Node ID 995cc683d95ccb028e0f349b3fc8dec01d8e29c0
# Parent  2bffdf62fe7fc67f2c1a946bc62706bb0814c69b
replaced swap by contrapos_np;

diff -r 2bffdf62fe7f -r 995cc683d95c src/HOLCF/FOCUS/Buffer_adm.ML
--- a/src/HOLCF/FOCUS/Buffer_adm.ML	Thu Dec 08 20:15:50 2005 +0100
+++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Thu Dec 08 20:15:57 2005 +0100
@@ -219,7 +219,7 @@
 b y Safe_tac;
 b y rewtac BufAC_Asm_F_def;
 b y Safe_tac;
-b y etac Classical.swap 1;
+b y etac contrapos_np 1;
 b y dtac (fstream_exhaust_eq RS iffD1) 1;
 b y Clarsimp_tac 1;
 b y datac fstream_lub_lemma 1 1;
@@ -230,7 +230,7 @@
 b y Clarify_tac 1;
 b y Simp_tac 1;
 b y rtac disjCI 1;
-b y etac Classical.swap 1;
+b y etac contrapos_np 1;
 b y dtac (fstream_exhaust_eq RS iffD1) 1;
 b y Clarsimp_tac 1;
 b y datac fstream_lub_lemma 1 1;
@@ -252,7 +252,7 @@
 by (rtac BufAC_Asm_def 1);
 b y rewtac BufAC_Asm_F_def;
 b y Safe_tac;
-b y etac Classical.swap 1;
+b y etac contrapos_np 1;
 b y dtac (fstream_exhaust_eq RS iffD1) 1;
 b y Clarsimp_tac 1;
 b y ftac fstream_prefix 1;
diff -r 2bffdf62fe7f -r 995cc683d95c src/HOLCF/FOCUS/Fstream.ML
--- a/src/HOLCF/FOCUS/Fstream.ML	Thu Dec 08 20:15:50 2005 +0100
+++ b/src/HOLCF/FOCUS/Fstream.ML	Thu Dec 08 20:15:57 2005 +0100
@@ -66,7 +66,7 @@
         "x << a~> z = (x = <> |  (? y. x = a~> y &  y << z))" (fn _ => [
         simp_tac(HOL_ss addsimps [fscons_def2, Def_not_UU RS thm "stream_prefix'"])1,
         Step_tac 1,
-         ALLGOALS(etac Classical.swap),
+         ALLGOALS(etac contrapos_np),
          fast_tac (HOL_cs addIs [refl_less] addEs [DefE]) 2,
         rtac Lift_cases 1,
          contr_tac 1,
@@ -139,7 +139,7 @@
         step_tac (HOL_cs addSEs [DefE]) 1,
         step_tac (HOL_cs addSEs [DefE]) 1,
         step_tac (HOL_cs addSEs [DefE]) 1,
-        etac Classical.swap 1,
+        etac contrapos_np 1,
         fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
 
 qed_goal "slen_fscons_less_eq" (the_context ())