67 |
67 |
68 (* equality *) |
68 (* equality *) |
69 (@{const_name HOL.eq}, K true), |
69 (@{const_name HOL.eq}, K true), |
70 |
70 |
71 (* numerals *) |
71 (* numerals *) |
72 (@{const_name zero_class.zero}, is_arithT_dom), |
72 (@{const_name zero_class.zero}, is_arithT), |
73 (@{const_name one_class.one}, is_arithT_dom), |
73 (@{const_name one_class.one}, is_arithT), |
74 (@{const_name Int.Pls}, K true), |
74 (@{const_name Int.Pls}, K true), |
75 (@{const_name Int.Min}, K true), |
75 (@{const_name Int.Min}, K true), |
76 (@{const_name Int.Bit0}, K true), |
76 (@{const_name Int.Bit0}, K true), |
77 (@{const_name Int.Bit1}, K true), |
77 (@{const_name Int.Bit1}, K true), |
78 (@{const_name number_of}, is_arithT_ran), |
78 (@{const_name number_of}, is_arithT_ran), |