Lines Matching defs:Const
11 fun Const s = prim_mk_const{Name=s, Thy="integer"};
13 val negate_tm = Const "int_neg"
14 val plus_tm = Const "int_add"
15 val minus_tm = Const "int_sub"
16 val mult_tm = Const "int_mul"
17 val exp_tm = Const "int_exp"
18 val div_tm = Const "int_div"
19 val mod_tm = Const "int_mod"
20 val quot_tm = Const "int_quot"
21 val rem_tm = Const "int_rem"
22 val less_tm = Const "int_lt"
23 val leq_tm = Const "int_le"
24 val great_tm = Const "int_gt"
25 val geq_tm = Const "int_ge"
26 val min_tm = Const "int_min"
27 val max_tm = Const "int_max";
28 val absval_tm = Const "ABS"
29 val divides_tm = Const "int_divides"
30 val LEAST_INT_tm = Const "LEAST_INT"
31 val int_injection = Const "int_of_num"
32 val Num_tm = Const "Num"