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