--- a/src/HOL/Word/Tools/smt2_word.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Word/Tools/smt2_word.ML Thu Jun 12 01:00:49 2014 +0200
@@ -9,12 +9,11 @@
open Word_Lib
+
(* SMT-LIB logic *)
fun smtlib_logic ts =
- if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts
- then SOME "QF_AUFBV"
- else NONE
+ if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "QF_AUFBV" else NONE
(* SMT-LIB builtins *)
@@ -141,4 +140,4 @@
SMTLIB2_Interface.add_logic (20, smtlib_logic) #>
setup_builtins))
-end
+end;