# HG changeset patch # User blanchet # Date 1393847300 -3600 # Node ID aa50d903e0a7d043f3dc7a513ff44314203f1ff8 # Parent 75907f171d4ce5b0af13314b0d9c685965ce4909 adapted example diff -r 75907f171d4c -r aa50d903e0a7 src/HOL/BNF_Comp.thy --- a/src/HOL/BNF_Comp.thy Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/BNF_Comp.thy Mon Mar 03 12:48:20 2014 +0100 @@ -147,7 +147,7 @@ ML_file "Tools/BNF/bnf_comp_tactics.ML" ML_file "Tools/BNF/bnf_comp.ML" -hide_const id_bnf_comp -hide_fact id_bnf_comp_def type_definition_id_bnf_comp_UNIV +hide_const (open) id_bnf_comp +hide_fact (open) id_bnf_comp_def type_definition_id_bnf_comp_UNIV end diff -r 75907f171d4c -r aa50d903e0a7 src/HOL/BNF_Examples/Stream.thy --- a/src/HOL/BNF_Examples/Stream.thy Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/BNF_Examples/Stream.thy Mon Mar 03 12:48:20 2014 +0100 @@ -33,16 +33,16 @@ assume "a \ set1_pre_stream (dtor_stream s)" then have "a = shd s" by (cases "dtor_stream s") - (auto simp: shd_def fsts_def set1_pre_stream_def stream.dtor_ctor SCons_def - Abs_stream_pre_stream_inverse Abs_stream_pre_stream_inject split: stream.splits) + (auto simp: BNF_Comp.id_bnf_comp_def shd_def fsts_def set1_pre_stream_def stream.dtor_ctor SCons_def + split: stream.splits) with Base show "P a s" by simp next fix a :: 'a and s' :: "'a stream" and s :: "'a stream" assume "s' \ set2_pre_stream (dtor_stream s)" and prems: "a \ sset s'" "P a s'" then have "s' = stl s" by (cases "dtor_stream s") - (auto simp: stl_def snds_def set2_pre_stream_def stream.dtor_ctor SCons_def - Abs_stream_pre_stream_inverse Abs_stream_pre_stream_inject split: stream.splits) + (auto simp: BNF_Comp.id_bnf_comp_def stl_def snds_def set2_pre_stream_def stream.dtor_ctor SCons_def + split: stream.splits) with Step prems show "P a s" by simp qed