author | wenzelm |
Tue, 10 Nov 2015 23:41:20 +0100 (2015-11-10) | |
changeset 61626 | c304402cc3df |
parent 61625 | 18e3efa15e52 |
child 61627 | 6059ce322766 |
child 61628 | 8dd2bd4fe30b |
src/HOL/SMT.thy | file | annotate | diff | comparison | revisions |
--- 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