equal
deleted
inserted
replaced
98 |
98 |
99 fun add_inj_const c = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} => |
99 fun add_inj_const c = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} => |
100 {splits = splits, inj_consts = update (op =) c inj_consts, |
100 {splits = splits, inj_consts = update (op =) c inj_consts, |
101 discrete = discrete}); |
101 discrete = discrete}); |
102 |
102 |
103 val (split_limit, setup_split_limit) = Attrib.config_int "linarith_split_limit" 9; |
103 val (split_limit, setup_split_limit) = Attrib.config_int "linarith_split_limit" (K 9); |
104 val (neq_limit, setup_neq_limit) = Attrib.config_int "linarith_neq_limit" 9; |
104 val (neq_limit, setup_neq_limit) = Attrib.config_int "linarith_neq_limit" (K 9); |
105 |
105 |
106 |
106 |
107 structure LA_Data = |
107 structure LA_Data = |
108 struct |
108 struct |
109 |
109 |