src/HOL/Library/Numeral_Type.thy
changeset 52147 9943f8067f11
parent 52143 36ffe23b25f8
child 55142 378ae9e46175
equal deleted inserted replaced
52146:ceb31e1ded30 52147:9943f8067f11
   517             Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
   517             Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
   518           end
   518           end
   519       | bit_tr' b _ = raise Match;
   519       | bit_tr' b _ = raise Match;
   520   in
   520   in
   521    [(@{type_syntax bit0}, K (bit_tr' 0)),
   521    [(@{type_syntax bit0}, K (bit_tr' 0)),
   522     (@{type_syntax bit1}, K (bit_tr' 1))] end;
   522     (@{type_syntax bit1}, K (bit_tr' 1))]
       
   523   end;
   523 *}
   524 *}
   524 
   525 
   525 subsection {* Examples *}
   526 subsection {* Examples *}
   526 
   527 
   527 lemma "CARD(0) = 0" by simp
   528 lemma "CARD(0) = 0" by simp