# HG changeset patch # User blanchet # Date 1379951003 -7200 # Node ID 4163160853fde047027a87d56e9faf4e8694af46 # Parent 58d1b63bea81e4f596635460d1ba9c51aa49807f added [code] to selectors diff -r 58d1b63bea81 -r 4163160853fd src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Mon Sep 23 14:53:43 2013 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Sep 23 17:43:23 2013 +0200 @@ -764,7 +764,7 @@ @{thm list.discI(1)[no_vars]} \\ @{thm list.discI(2)[no_vars]} -\item[@{text "t."}\hthm{sel} @{text "[simp]"}\rm:] ~ \\ +\item[@{text "t."}\hthm{sel} @{text "[simp, code]"}\rm:] ~ \\ @{thm list.sel(1)[no_vars]} \\ @{thm list.sel(2)[no_vars]} diff -r 58d1b63bea81 -r 4163160853fd src/HOL/BNF/Examples/Stream.thy --- a/src/HOL/BNF/Examples/Stream.thy Mon Sep 23 14:53:43 2013 +0200 +++ b/src/HOL/BNF/Examples/Stream.thy Mon Sep 23 17:43:23 2013 +0200 @@ -33,7 +33,6 @@ *} code_datatype Stream -lemmas [code] = stream.sel stream.set stream.case lemma stream_case_cert: assumes "CASE \ stream_case c" @@ -66,8 +65,6 @@ "shd (smap f s) = f (shd s)" "stl (smap f s) = smap f (stl s)" by (case_tac [!] s) auto -declare stream.map[code] - theorem shd_sset: "shd s \ sset s" by (case_tac s) auto diff -r 58d1b63bea81 -r 4163160853fd src/HOL/BNF/Tools/bnf_ctr_sugar.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Mon Sep 23 14:53:43 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Mon Sep 23 17:43:23 2013 +0200 @@ -772,7 +772,7 @@ (expandN, expand_thms, []), (injectN, inject_thms, iff_attrs @ induct_simp_attrs), (nchotomyN, [nchotomy_thm], []), - (selN, all_sel_thms, simp_attrs), + (selN, all_sel_thms, code_simp_attrs), (splitN, [split_thm], []), (split_asmN, [split_asm_thm], []), (splitsN, [split_thm, split_asm_thm], []),