47 (@{const HOL.implies}, "=>"), |
47 (@{const HOL.implies}, "=>"), |
48 (@{const HOL.eq ('a)}, "="), |
48 (@{const HOL.eq ('a)}, "="), |
49 (@{const If ('a)}, "ite"), |
49 (@{const If ('a)}, "ite"), |
50 (@{const less (int)}, "<"), |
50 (@{const less (int)}, "<"), |
51 (@{const less_eq (int)}, "<="), |
51 (@{const less_eq (int)}, "<="), |
52 (@{const uminus (int)}, "~"), |
52 (@{const uminus (int)}, "-"), |
53 (@{const plus (int)}, "+"), |
53 (@{const plus (int)}, "+"), |
54 (@{const minus (int)}, "-")] #> |
54 (@{const minus (int)}, "-")] #> |
55 SMT2_Builtin.add_builtin_fun smtlib2C |
55 SMT2_Builtin.add_builtin_fun smtlib2C |
56 (Term.dest_Const @{const times (int)}, times) |
56 (Term.dest_Const @{const times (int)}, times) |
57 |
57 |