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.
removed needless comment (yes, sum_case_if is needed)
authorblanchet
Tue, 28 May 2013 08:36:11 +0200
changeset 52194 6289b167bbab
parent 52193 014d6b3f5792
child 52195 056ec8201667
removed needless comment (yes, sum_case_if is needed)
src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Tue May 28 08:29:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Tue May 28 08:36:11 2013 +0200
@@ -108,7 +108,6 @@
   unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_comp's @
     map_ids'' @ iter_unfold_thms) THEN rtac refl 1;
 
-(*TODO: sum_case_if needed?*)
 val coiter_unfold_thms =
   @{thms id_def ident_o_ident sum_case_if sum_case_o_inj} @ sum_prod_thms_map;
isabelle