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.
merged
authortraytel
Wed, 14 Feb 2024 08:31:24 +0100
changeset 79596 1b3770369ee7
parent 79595 3e27ab965a36 (diff)
parent 79594 f933e9153624 (current diff)
child 79600 d9eb4807557c
child 79601 3430787e0620
child 79611 97612262718a
merged
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Tue Feb 13 16:03:55 2024 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Wed Feb 14 08:31:24 2024 +0100
@@ -139,6 +139,8 @@
     eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN'
     assume_tac ctxt ORELSE'
     etac ctxt notE THEN' assume_tac ctxt ORELSE'
+    (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (
+      map (Local_Defs.unfold0 ctxt @{thms id_def[symmetric]}) map_ident0s @ map_comps))) ORELSE'
     (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
          sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @
        map_ident0s @ map_comps))) ORELSE'
isabelle