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/Sprod0.ML
changeset 4535 f24cebc299e4
parent 2640 ee4dfce170a0
child 4833 2e53109d4bc8 
--- a/src/HOLCF/Sprod0.ML	Thu Jan 08 18:08:43 1998 +0100
+++ b/src/HOLCF/Sprod0.ML	Thu Jan 08 18:09:07 1998 +0100
@@ -207,7 +207,7 @@
 (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (rtac  select_equality 1),
+        (rtac select_equality 1),
         (rtac conjI 1),
         (fast_tac HOL_cs  1),
         (strip_tac 1),
@@ -242,7 +242,7 @@
 (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (rtac  select_equality 1),
+        (rtac select_equality 1),
         (rtac conjI 1),
         (fast_tac HOL_cs  1),
         (strip_tac 1),
@@ -275,7 +275,7 @@
 (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (rtac  select_equality 1),
+        (rtac select_equality 1),
         (rtac conjI 1),
         (strip_tac 1),
         (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
@@ -295,7 +295,7 @@
 (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (rtac  select_equality 1),
+        (rtac select_equality 1),
         (rtac conjI 1),
         (strip_tac 1),
         (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
isabelle