# HG changeset patch # User blanchet # Date 1379932834 -7200 # Node ID 6a4e3299dfd17e6d5a428a066d4ddd1f48914258 # Parent 576f9637dc7a10dd974bbf397639bc0e5a8d0016 set [code] on case equations diff -r 576f9637dc7a -r 6a4e3299dfd1 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Mon Sep 23 10:58:37 2013 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Sep 23 12:40:34 2013 +0200 @@ -729,7 +729,7 @@ \begin{indentblock} \begin{description} -\item[@{text "t."}\hthm{case} @{text "[simp]"}\rm:] ~ \\ +\item[@{text "t."}\hthm{case} @{text "[simp, code]"}\rm:] ~ \\ @{thm list.case(1)[no_vars]} \\ @{thm list.case(2)[no_vars]} @@ -802,19 +802,19 @@ \begin{indentblock} \begin{description} -\item[@{text "t."}\hthm{set} @{text "[code]"}\rm:] ~ \\ +\item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\ @{thm list.set(1)[no_vars]} \\ @{thm list.set(2)[no_vars]} -\item[@{text "t."}\hthm{map} @{text "[code]"}\rm:] ~ \\ +\item[@{text "t."}\hthm{map} @{text "[simp, code]"}\rm:] ~ \\ @{thm list.map(1)[no_vars]} \\ @{thm list.map(2)[no_vars]} -\item[@{text "t."}\hthm{rel\_inject} @{text "[code]"}\rm:] ~ \\ +\item[@{text "t."}\hthm{rel\_inject} @{text "[simp, code]"}\rm:] ~ \\ @{thm list.rel_inject(1)[no_vars]} \\ @{thm list.rel_inject(2)[no_vars]} -\item[@{text "t."}\hthm{rel\_distinct} @{text "[code]"}\rm:] ~ \\ +\item[@{text "t."}\hthm{rel\_distinct} @{text "[simp, code]"}\rm:] ~ \\ @{thm list.rel_distinct(1)[no_vars]} \\ @{thm list.rel_distinct(2)[no_vars]} @@ -839,11 +839,11 @@ Given $m > 1$ mutually recursive datatypes, this induction rule can be used to prove $m$ properties simultaneously. -\item[@{text "t."}\hthm{fold} @{text "[code]"}\rm:] ~ \\ +\item[@{text "t."}\hthm{fold} @{text "[simp, code]"}\rm:] ~ \\ @{thm list.fold(1)[no_vars]} \\ @{thm list.fold(2)[no_vars]} -\item[@{text "t."}\hthm{rec} @{text "[code]"}\rm:] ~ \\ +\item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\ @{thm list.rec(1)[no_vars]} \\ @{thm list.rec(2)[no_vars]} diff -r 576f9637dc7a -r 6a4e3299dfd1 src/HOL/BNF/Tools/bnf_ctr_sugar.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Mon Sep 23 10:58:37 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Mon Sep 23 12:40:34 2013 +0200 @@ -133,6 +133,7 @@ val iff_attrs = @{attributes [iff]}; val induct_simp_attrs = @{attributes [induct_simp]}; val simp_attrs = @{attributes [simp]}; +val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs; fun unflat_lookup eq xs ys = map (fn xs' => permute_like eq xs xs' ys); @@ -758,7 +759,7 @@ val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name)); val notes = - [(caseN, case_thms, simp_attrs), + [(caseN, case_thms, code_simp_attrs), (case_congN, [case_cong_thm], []), (case_convN, case_conv_thms, []), (collapseN, safe_collapse_thms, simp_attrs),