| changeset 56645 | a16d294f7e3f |
| parent 56643 | 41d3596d8a64 |
| child 56650 | 1f9ab71d43a5 |
| 56644:efb39e0a89b0 | 56645:a16d294f7e3f |
|---|---|
239 @{thms sum_size_o_map} |
239 @{thms sum_size_o_map} |
240 #> BNF_LFP_Size.register_size @{type_name prod} @{const_name prod_size} @{thms prod.size} |
240 #> BNF_LFP_Size.register_size @{type_name prod} @{const_name prod_size} @{thms prod.size} |
241 @{thms prod_size_o_map} |
241 @{thms prod_size_o_map} |
242 *} |
242 *} |
243 |
243 |
244 |
|
245 hide_fact (open) id_transfer |
244 hide_fact (open) id_transfer |
246 |
245 |
247 end |
246 end |