full path
authorblanchet
Tue Mar 11 15:34:38 2014 +0100 (2014-03-11)
changeset 56046683148f3ae48
parent 56045 1ca060139a59
child 56047 1f283d0a4966
full path
src/HOL/SMT.thy
src/HOL/SMT_Examples/SMT_Word_Examples.thy
     1.1 --- a/src/HOL/SMT.thy	Tue Mar 11 11:32:32 2014 +0100
     1.2 +++ b/src/HOL/SMT.thy	Tue Mar 11 15:34:38 2014 +0100
     1.3 @@ -425,7 +425,6 @@
     1.4    by auto
     1.5  
     1.6  
     1.7 -
     1.8  hide_type (open) pattern
     1.9  hide_const Pattern fun_app term_true term_false z3div z3mod
    1.10  hide_const (open) trigger pat nopat weight
     2.1 --- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Tue Mar 11 11:32:32 2014 +0100
     2.2 +++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Tue Mar 11 15:34:38 2014 +0100
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* Word examples for for SMT binding *}
     2.5  
     2.6  theory SMT_Word_Examples
     2.7 -imports Word
     2.8 +imports "~~/src/HOL/Word/Word"
     2.9  begin
    2.10  
    2.11  declare [[smt_oracle = true]]