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/UNITY/Constrains.thy
changeset 21687 f689f729afab
parent 21588 cd0dc678a205
child 23543 12271cfad085 
--- a/src/ZF/UNITY/Constrains.thy	Wed Dec 06 21:19:03 2006 +0100
+++ b/src/ZF/UNITY/Constrains.thy	Thu Dec 07 00:42:04 2006 +0100
@@ -546,7 +546,7 @@
                                    constrains_imp_Constrains] 1),
               rtac constrainsI 1,
               (* Three subgoals *)
-              rewrite_goal_tac [st_set_def] 3,
+              Goal.rewrite_goal_tac [st_set_def] 3,
               REPEAT (Force_tac 2),
               full_simp_tac (ss addsimps !program_defs_ref) 1,
               ALLGOALS (clarify_tac cs),
isabelle