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/HOL/Relation.ML
changeset 3718 d78cf498a88c
parent 3439 54785105178c
child 4089 96fba19bcbe2 
--- a/src/HOL/Relation.ML	Fri Sep 26 10:12:04 1997 +0200
+++ b/src/HOL/Relation.ML	Fri Sep 26 10:21:14 1997 +0200
@@ -164,7 +164,7 @@
     "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"
  (fn major::prems=>
   [ (rtac (major RS CollectE) 1),
-    (Step_tac 1),
+    (Clarify_tac 1),
     (rtac (hd prems) 1),
     (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
isabelle