clean up list of theorems
authorblanchet
Tue May 28 08:36:12 2013 +0200 (2013-05-28)
changeset 52195056ec8201667
parent 52194 6289b167bbab
child 52196 2281f33e8da6
clean up list of theorems
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 28 08:36:11 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 28 08:36:12 2013 +0200
     1.3 @@ -1018,9 +1018,8 @@
     1.4        ||>> mk_TFrees nn
     1.5        ||>> variant_tfrees fp_b_names;
     1.6  
     1.7 -    (* TODO: cleaner handling of fake contexts, without "background_theory" *)
     1.8 -    (*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a
     1.9 -      locale and shadows an existing global type*)
    1.10 +    (* TODO: Cleaner handling of fake contexts, without "background_theory". The case where the new
    1.11 +       type is defined in a locale and shadows an existing global type is currently not handled. *)
    1.12  
    1.13      fun add_fake_type spec =
    1.14        Sign.add_type no_defs_lthy (type_binding_of spec,
     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Tue May 28 08:36:11 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Tue May 28 08:36:12 2013 +0200
     2.3 @@ -99,10 +99,9 @@
     2.4    unfold_thms_tac ctxt [ctr_def] THEN rtac (ctor_inject RS ssubst) 1 THEN
     2.5    unfold_thms_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
     2.6  
     2.7 -(*TODO: Try "sum_prod_thms_map" here, enriched with a few theorems*)
     2.8  val iter_unfold_thms =
     2.9 -  @{thms comp_def convol_def fst_conv id_def map_pair_simp prod_case_Pair_iden snd_conv split_conv
    2.10 -      sum.simps(5,6) sum_map.simps unit_case_Unity};
    2.11 +  @{thms comp_def convol_def fst_conv id_def prod_case_Pair_iden snd_conv
    2.12 +      split_conv unit_case_Unity} @ sum_prod_thms_map;
    2.13  
    2.14  fun mk_iter_tac pre_map_defs map_comp's map_ids'' iter_defs ctor_iter ctr_def ctxt =
    2.15    unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_comp's @