equal
deleted
inserted
replaced
66 "various arithmetic decision procedures"; |
66 "various arithmetic decision procedures"; |
67 |
67 |
68 |
68 |
69 (* some specialized syntactic operations *) |
69 (* some specialized syntactic operations *) |
70 |
70 |
71 fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n; |
71 fun mk_number T 1 = HOLogic.numeral_const T $ HOLogic.one_const |
|
72 | mk_number T n = HOLogic.mk_number T n; |
72 |
73 |
73 val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; |
74 val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; |
74 |
75 |
75 fun mk_minus t = |
76 fun mk_minus t = |
76 let val T = Term.fastype_of t |
77 let val T = Term.fastype_of t |