src/HOL/Library/positivstellensatz.ML
changeset 39920 7479334d2c90
parent 39027 e4262f9e6a4e
child 44058 ae85c5d64913
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Mon Oct 04 14:46:49 2010 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Fri May 07 15:36:03 2010 +0200
     1.3 @@ -270,7 +270,7 @@
     1.4    by (atomize (full)) (cases "x <= y", auto simp add: min_def)};
     1.5  
     1.6  
     1.7 -         (* Miscalineous *)
     1.8 +         (* Miscellaneous *)
     1.9  fun literals_conv bops uops cv = 
    1.10   let fun h t =
    1.11    case (term_of t) of