src/HOL/Tools/SMT/smt_builtin.ML
2010-11-24 boehmes 2010-11-24 swap names for built-in tester functions (to better reflect the intuition of what they do); eta-expand all built-in functions (even those which are only partially supported)
2010-11-24 boehmes 2010-11-24 be more precise: only treat constant 'distinct' applied to an explicit list as built-in
2010-11-23 blanchet 2010-11-23 more precise characterization of built-in constants "number_of", "0", and "1"
2010-11-22 boehmes 2010-11-22 added support for quantifier weight annotations
2010-10-29 boehmes 2010-10-29 added crafted list of SMT built-in constants