138 in mk_binary' n T \<^typ>\<open>HOL.bool\<close> t1 t2 end |
138 in mk_binary' n T \<^typ>\<open>HOL.bool\<close> t1 t2 end |
139 |
139 |
140 fun mk_less t1 t2 = mk_binary_pred \<^const_name>\<open>ord_class.less\<close> \<^sort>\<open>linorder\<close> t1 t2 |
140 fun mk_less t1 t2 = mk_binary_pred \<^const_name>\<open>ord_class.less\<close> \<^sort>\<open>linorder\<close> t1 t2 |
141 fun mk_less_eq t1 t2 = mk_binary_pred \<^const_name>\<open>ord_class.less_eq\<close> \<^sort>\<open>linorder\<close> t1 t2 |
141 fun mk_less_eq t1 t2 = mk_binary_pred \<^const_name>\<open>ord_class.less_eq\<close> \<^sort>\<open>linorder\<close> t1 t2 |
142 |
142 |
143 fun core_term_parser (SMTLIB.Sym "true", _) = SOME @{const HOL.True} |
143 fun core_term_parser (SMTLIB.Sym "true", _) = SOME \<^const>\<open>HOL.True\<close> |
144 | core_term_parser (SMTLIB.Sym "false", _) = SOME @{const HOL.False} |
144 | core_term_parser (SMTLIB.Sym "false", _) = SOME \<^const>\<open>HOL.False\<close> |
145 | core_term_parser (SMTLIB.Sym "not", [t]) = SOME (HOLogic.mk_not t) |
145 | core_term_parser (SMTLIB.Sym "not", [t]) = SOME (HOLogic.mk_not t) |
146 | core_term_parser (SMTLIB.Sym "and", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_conj) t ts) |
146 | core_term_parser (SMTLIB.Sym "and", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_conj) t ts) |
147 | core_term_parser (SMTLIB.Sym "or", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_disj) t ts) |
147 | core_term_parser (SMTLIB.Sym "or", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_disj) t ts) |
148 | core_term_parser (SMTLIB.Sym "=>", [t1, t2]) = SOME (HOLogic.mk_imp (t1, t2)) |
148 | core_term_parser (SMTLIB.Sym "=>", [t1, t2]) = SOME (HOLogic.mk_imp (t1, t2)) |
149 | core_term_parser (SMTLIB.Sym "implies", [t1, t2]) = SOME (HOLogic.mk_imp (t1, t2)) |
149 | core_term_parser (SMTLIB.Sym "implies", [t1, t2]) = SOME (HOLogic.mk_imp (t1, t2)) |