# HG changeset patch # User haftmann # Date 1265788165 -3600 # Node ID 96a21dd3b34929d706b0dfbb6ad21e0cad6f9c54 # Parent 894e82be8d05ccb8b7390dfa0e967655c1610b7b rely less on ordered rewriting diff -r 894e82be8d05 -r 96a21dd3b349 src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Tue Feb 09 16:07:09 2010 +0100 +++ b/src/HOL/Decision_Procs/Approximation.thy Wed Feb 10 08:49:25 2010 +0100 @@ -2950,7 +2950,8 @@ (\ i = 0.. j \ {k.. j \ {k.. {real l .. real u}" . } thus ?thesis using DERIV by blast qed