diff -r 4f54d2759a0b -r a9c0572109af src/HOL/SMT.thy
--- 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