# HG changeset patch
# User blanchet
# Date 1394548478 -3600
# Node ID 683148f3ae48aa23da60c7461bb7be78527fe119
# Parent  1ca060139a59c6917d440524a7f74d2083da2da1
full path

diff -r 1ca060139a59 -r 683148f3ae48 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Tue Mar 11 11:32:32 2014 +0100
+++ b/src/HOL/SMT.thy	Tue Mar 11 15:34:38 2014 +0100
@@ -425,7 +425,6 @@
   by auto
 
 
-
 hide_type (open) pattern
 hide_const Pattern fun_app term_true term_false z3div z3mod
 hide_const (open) trigger pat nopat weight
diff -r 1ca060139a59 -r 683148f3ae48 src/HOL/SMT_Examples/SMT_Word_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Tue Mar 11 11:32:32 2014 +0100
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Tue Mar 11 15:34:38 2014 +0100
@@ -5,7 +5,7 @@
 header {* Word examples for for SMT binding *}
 
 theory SMT_Word_Examples
-imports Word
+imports "~~/src/HOL/Word/Word"
 begin
 
 declare [[smt_oracle = true]]