src/HOL/Tools/SMT/z3_real.ML
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-06-01 haftmann 2015-06-01 separate class for division operator, with particular syntax added in more specific classes
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'