1.1 --- a/src/HOL/SMT/Tools/z3_interface.ML	Wed May 12 23:54:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,35 +0,0 @@
     1.4 -(*  Title:      HOL/SMT/Tools/z3_interface.ML
     1.5 -    Author:     Sascha Boehme, TU Muenchen
     1.6 -
     1.7 -Interface to Z3 based on a relaxed version of SMT-LIB.
     1.8 -*)
     1.9 -
    1.10 -signature Z3_INTERFACE =
    1.11 -sig
    1.12 -  val interface: string list -> SMT_Translate.config
    1.13 -end
    1.14 -
    1.15 -structure Z3_Interface: Z3_INTERFACE =
    1.16 -struct
    1.17 -
    1.18 -fun z3_builtin_fun bf c ts =
    1.19 -  (case Const c of
    1.20 -    @{term "op / :: real => _"} => SOME ("/", ts)
    1.21 -  | _ => bf c ts)
    1.22 -
    1.23 -fun interface comments =
    1.24 -  let
    1.25 -    val {prefixes, strict, builtins, serialize} =
    1.26 -      SMTLIB_Interface.interface comments
    1.27 -    val {builtin_typ, builtin_num, builtin_fun} = builtins
    1.28 -  in
    1.29 -   {prefixes = prefixes,
    1.30 -    strict = strict,
    1.31 -    builtins = {
    1.32 -      builtin_typ = builtin_typ,
    1.33 -      builtin_num = builtin_num,
    1.34 -      builtin_fun = z3_builtin_fun builtin_fun},
    1.35 -    serialize = serialize}
    1.36 -  end
    1.37 -
    1.38 -end