Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/SMT/smt_builtin.ML
changeset 40691 a68f64f99832
parent 40686 4725ed462387
child 41059 d2b1fc1b8e19 
--- a/src/HOL/Tools/SMT/smt_builtin.ML	Thu Nov 25 00:17:16 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Thu Nov 25 00:32:30 2010 +0100
@@ -69,8 +69,8 @@
   (@{const_name HOL.eq}, K true),
 
   (* numerals *)
-  (@{const_name zero_class.zero}, is_arithT_dom),
-  (@{const_name one_class.one}, is_arithT_dom),
+  (@{const_name zero_class.zero}, is_arithT),
+  (@{const_name one_class.one}, is_arithT),
   (@{const_name Int.Pls}, K true),
   (@{const_name Int.Min}, K true),
   (@{const_name Int.Bit0}, K true),
isabelle