# HG changeset patch
# User wenzelm
# Date 1447195280 -3600
# Node ID c304402cc3df3699a290c2f764ffc3701faa9f41
# Parent  18e3efa15e52166003162ff68f282d13326ed50b
recovered from a9c0572109af;

diff -r 18e3efa15e52 -r c304402cc3df src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Tue Nov 10 23:39:50 2015 +0100
+++ b/src/HOL/SMT.thy	Tue Nov 10 23:41:20 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Sascha Boehme, TU Muenchen
 *)
 
-section \<open>Bi ndings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\<close>
+section \<open>Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\<close>
 
 theory SMT
 imports Divides