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.
avoid unsound 'nitpick_simp' attribute on nonterminating, nonproductive equations
authorblanchet
Tue, 06 Oct 2015 21:04:44 +0200
changeset 61347 2ebdd603cd71
parent 61346 a696414fa3a1
child 61348 d7215449be83
avoid unsound 'nitpick_simp' attribute on nonterminating, nonproductive equations
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Oct 06 19:35:33 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Oct 06 21:04:44 2015 +0200
@@ -1102,7 +1102,7 @@
            (rel_injectN, rel_inject_thms, K simp_attrs),
            (rel_introsN, rel_intro_thms, K []),
            (rel_selN, rel_sel_thms, K []),
-           (setN, set_thms, K (code_attrs @ nitpicksimp_attrs @ simp_attrs)),
+           (setN, set_thms, K (code_attrs @ case_fp fp nitpicksimp_attrs [] @ simp_attrs)),
            (set_casesN, set_cases_thms, nth set_cases_attrss),
            (set_introsN, set_intros_thms, K []),
            (set_selN, set_sel_thms, K [])]
isabelle