--- 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;
--- 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 ())