changeset 58368 | fe083c681ed8 |
parent 58301 | de95aeedf49e |
child 58881 | b9556a055632 |
--- a/src/HOL/Library/RBT_Set.thy Thu Sep 18 00:03:46 2014 +0200 +++ b/src/HOL/Library/RBT_Set.thy Thu Sep 18 15:07:43 2014 +0200 @@ -88,6 +88,9 @@ "setsum = setsum" .. lemma [code, code del]: + "setprod = setprod" .. + +lemma [code, code del]: "Product_Type.product = Product_Type.product" .. lemma [code, code del]: