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