Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
rewrite_goal_tac;
authorwenzelm
Tue, 03 Jul 2007 17:17:17 +0200
changeset 23543 12271cfad085
parent 23542 61ffcf4c02c7
child 23544 4b4165cb3e0d
rewrite_goal_tac;
src/ZF/UNITY/Constrains.thy file | annotate | diff | comparison | revisions 
--- a/src/ZF/UNITY/Constrains.thy	Tue Jul 03 17:17:16 2007 +0200
+++ b/src/ZF/UNITY/Constrains.thy	Tue Jul 03 17:17:17 2007 +0200
@@ -546,7 +546,7 @@
                                    constrains_imp_Constrains] 1),
               rtac constrainsI 1,
               (* Three subgoals *)
-              Goal.rewrite_goal_tac [st_set_def] 3,
+              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