--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 04 13:02:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 04 13:02:28 2012 +0200
@@ -64,8 +64,10 @@
no_defs_lthy =
let
(* TODO: sanity checks on arguments *)
-
- (* TODO: normalize types of constructors w.r.t. each other *)
+ (* TODO: attributes (simp, case_names, etc.) *)
+ (* TODO: case syntax *)
+ (* TODO: integration with function package ("size") *)
+ (* TODO: omission of needless discriminators *)
val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
val caseof0 = prep_term no_defs_lthy raw_caseof;
@@ -379,9 +381,6 @@
(split_thm, split_asm_thm)
end;
- (* TODO: case syntax *)
- (* TODO: attributes (simp, case_names, etc.) *)
-
val notes =
[(case_congN, [case_cong_thm]),
(case_discsN, [case_disc_thm]),