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/ZF/ex/Commutation.ML
changeset 12484 7ad150f5fc10
parent 11316 b4e71bd751e4 
--- a/src/ZF/ex/Commutation.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/ZF/ex/Commutation.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -28,7 +28,7 @@
 (* A special case of square_rtrancl_on *)
 Goalw [diamond_def, commute_def, strip_def]
  "diamond(r) ==> strip(r)";
-by (resolve_tac [square_rtrancl] 1);
+by (rtac square_rtrancl 1);
 by (ALLGOALS(Asm_simp_tac));
 qed "diamond_strip";
 
@@ -116,7 +116,7 @@
 Goalw [confluent_def, Church_Rosser_def, square_def,commute_def,diamond_def]  
 "confluent(r) ==> Church_Rosser(r)";
 by Auto_tac;
-by (forward_tac [fieldI1] 1);
+by (ftac fieldI1 1);
 by (full_simp_tac (simpset() addsimps [rtrancl_field]) 1);
 by (etac rtrancl_induct 1);
 by (ALLGOALS(Clarify_tac));
isabelle