src/HOL/Library/Quadratic_Discriminant.thy
changeset 73740 c46ff0efa1ce
parent 68553 333998becebe
equal deleted inserted replaced
73739:3e44f8c3f059 73740:c46ff0efa1ce