exposed fast_arith_neq_limit
authornipkow
Fri, 02 Apr 2004 17:40:32 +0200
changeset 14517 7ae3b247c6e9
parent 14516 a183dec876ab
child 14518 c3019a66180f
exposed fast_arith_neq_limit
src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Fri Apr 02 17:37:45 2004 +0200
+++ b/src/HOL/arith_data.ML	Fri Apr 02 17:40:32 2004 +0200
@@ -365,7 +365,8 @@
 
 val fast_arith_tac    = Fast_Arith.lin_arith_tac false
 and fast_ex_arith_tac = Fast_Arith.lin_arith_tac
-and trace_arith    = Fast_Arith.trace;
+and trace_arith    = Fast_Arith.trace
+and fast_arith_neq_limit = Fast_Arith.fast_arith_neq_limit;
 
 local