changeset 32843 | c8f5a7c8353f |
parent 32829 | 671eb46eb0a3 |
child 33002 | f3f02f36a3e2 |
--- a/src/HOL/Library/positivstellensatz.ML Thu Oct 01 22:40:29 2009 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Thu Oct 01 23:27:05 2009 +0200 @@ -538,7 +538,7 @@ val nnf_norm_conv' = nnf_conv then_conv literals_conv [@{term "op &"}, @{term "op |"}] [] - (More_Conv.cache_conv + (Conv.cache_conv (first_conv [real_lt_conv, real_le_conv, real_eq_conv, real_not_lt_conv, real_not_le_conv, real_not_eq_conv, all_conv]))