equal
deleted
inserted
replaced
53 |
53 |
54 (* technicalities *) |
54 (* technicalities *) |
55 (@{const_name SMT.pat}, K true), |
55 (@{const_name SMT.pat}, K true), |
56 (@{const_name SMT.nopat}, K true), |
56 (@{const_name SMT.nopat}, K true), |
57 (@{const_name SMT.trigger}, K true), |
57 (@{const_name SMT.trigger}, K true), |
|
58 (@{const_name SMT.weight}, K true), |
58 (@{const_name SMT.fun_app}, K true), |
59 (@{const_name SMT.fun_app}, K true), |
59 (@{const_name SMT.z3div}, K true), |
60 (@{const_name SMT.z3div}, K true), |
60 (@{const_name SMT.z3mod}, K true), |
61 (@{const_name SMT.z3mod}, K true), |
61 |
62 |
62 (* equality *) |
63 (* equality *) |