equal
deleted
inserted
replaced
103 let val (t1,t2) = dest_plus t |
103 let val (t1,t2) = dest_plus t |
104 in dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts))) end |
104 in dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts))) end |
105 handle TERM _ => (k, t::ts); |
105 handle TERM _ => (k, t::ts); |
106 |
106 |
107 (*Code for testing whether numerals are already used in the goal*) |
107 (*Code for testing whether numerals are already used in the goal*) |
108 fun is_numeral (Const(@{const_name Numeral.number_of}, _) $ w) = true |
108 fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true |
109 | is_numeral _ = false; |
109 | is_numeral _ = false; |
110 |
110 |
111 fun prod_has_numeral t = exists is_numeral (dest_prod t); |
111 fun prod_has_numeral t = exists is_numeral (dest_prod t); |
112 |
112 |
113 (*The Sucs found in the term are converted to a binary numeral. If relaxed is false, |
113 (*The Sucs found in the term are converted to a binary numeral. If relaxed is false, |