changeset 52147 | 9943f8067f11 |
parent 52143 | 36ffe23b25f8 |
child 55142 | 378ae9e46175 |
--- a/src/HOL/Library/Numeral_Type.thy Sat May 25 17:13:34 2013 +0200 +++ b/src/HOL/Library/Numeral_Type.thy Sat May 25 17:40:44 2013 +0200 @@ -519,7 +519,8 @@ | bit_tr' b _ = raise Match; in [(@{type_syntax bit0}, K (bit_tr' 0)), - (@{type_syntax bit1}, K (bit_tr' 1))] end; + (@{type_syntax bit1}, K (bit_tr' 1))] + end; *} subsection {* Examples *}