changeset 61611 | a9c0572109af |
parent 60758 | d8d85a8172b5 |
child 61626 | c304402cc3df |
--- a/src/HOL/SMT.thy Tue Nov 10 14:43:29 2015 +0000 +++ b/src/HOL/SMT.thy Tue Nov 10 17:49:54 2015 +0100 @@ -2,7 +2,7 @@ Author: Sascha Boehme, TU Muenchen *) -section \<open>Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\<close> +section \<open>Bi ndings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\<close> theory SMT imports Divides