generate 'size_gen' for datatypes
authordesharna
Tue, 21 Oct 2014 17:23:13 +0200
changeset 58736 552ccec3f00f
parent 58735 919186869943
child 58737 b45405874f8f
generate 'size_gen' for datatypes
src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Oct 21 17:23:13 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Oct 21 17:23:13 2014 +0200
@@ -23,6 +23,7 @@
 
 val size_N = "size_";
 val sizeN = "size";
+val size_genN = "size_gen";
 val size_o_mapN = "size_o_map";
 
 val nitpicksimp_attrs = @{attributes [nitpick_simp]};
@@ -250,6 +251,7 @@
       val overloaded_size_simpss =
         map2 (map o derive_overloaded_size_simp) overloaded_size_defs' size_simpss;
       val size_thmss = map2 append size_simpss overloaded_size_simpss;
+      val size_gen_thmss = size_simpss
 
       val ABs = As ~~ Bs;
       val g_names = variant_names num_As "g";
@@ -315,6 +317,7 @@
 
       val notes =
         [(sizeN, size_thmss, code_attrs :: nitpicksimp_attrs @ simp_attrs),
+         (size_genN, size_gen_thmss, []),
          (size_o_mapN, size_o_map_thmss, [])]
         |> massage_multi_notes;