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/Tools/BNF/bnf_def_tactics.ML
changeset 55414 eab03e9cee8a
parent 55197 5a54ed681ba2
child 55642 63beb38e9258 
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Wed Feb 12 08:35:57 2014 +0100
@@ -265,7 +265,7 @@
           rtac (thm RS ord_eq_le_trans) THEN' etac @{thm subset_trans[OF image_mono Un_upper1]})
         set_maps,
         rtac sym,
-        rtac (box_equals OF [map_cong0 OF replicate live @{thm fun_cong[OF sum_case_o_inj(1)]},
+        rtac (box_equals OF [map_cong0 OF replicate live @{thm fun_cong[OF case_sum_o_inj(1)]},
            map_comp RS sym, map_id])] 1
   end;
isabelle