Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/FOCUS/Fstream.ML
changeset 18373 995cc683d95c
parent 18368 2f9b2539c5bb 
--- 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 ())
isabelle