Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
changeset 60867 86e7560e07d0
parent 60818 5e11a6e2b044
child 63198 c583ca33076a 
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Thu Aug 06 23:56:48 2015 +0200
@@ -1045,7 +1045,7 @@
       let
         val simp_ctxt =
           ctxt addsimps @{thms field_simps}
-          addsimps [@{thm nonzero_power_divide}, @{thm power_divide}]
+          addsimps [@{thm power_divide}]
         val th =
           Thm.instantiate' [] [SOME d, SOME (Thm.dest_arg P)]
             (if ord then @{lemma "(d=0 --> P) & (d>0 --> P) & (d<(0::real) --> P) ==> P" by auto}
isabelle