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/Sprod2.ML
changeset 7499 23e090051cb8
parent 4721 c8a8482a8124
child 9245 428385c4bc50 
--- a/src/HOLCF/Sprod2.ML	Mon Sep 06 22:12:08 1999 +0200
+++ b/src/HOLCF/Sprod2.ML	Tue Sep 07 10:40:58 1999 +0200
@@ -47,7 +47,7 @@
         (strip_tac 1),
         (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1),
         (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
-        (forward_tac [notUU_I] 1),
+        (ftac notUU_I 1),
         (atac 1),
         (REPEAT(asm_simp_tac(Sprod0_ss 
                 addsimps[inst_sprod_po,refl_less,minimal]) 1))
@@ -59,7 +59,7 @@
         (strip_tac 1),
         (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
         (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1),
-        (forward_tac [notUU_I] 1),
+        (ftac notUU_I 1),
         (atac 1),
         (REPEAT(asm_simp_tac(Sprod0_ss 
                 addsimps[inst_sprod_po,refl_less,minimal]) 1))
isabelle