src/HOL/Library/Quadratic_Discriminant.thy
changeset 62058 1cfd5d604937
parent 60500 903bb1495239
child 63465 d7610beb98bc
     1.1 --- a/src/HOL/Library/Quadratic_Discriminant.thy	Tue Jan 05 13:41:29 2016 +0100
     1.2 +++ b/src/HOL/Library/Quadratic_Discriminant.thy	Tue Jan 05 13:48:51 2016 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:       Roots of real quadratics
     1.5 +(*  Title:       HOL/Library/Quadratic_Discriminant.thy
     1.6      Author:      Tim Makarios <tjm1983 at gmail.com>, 2012
     1.7  
     1.8  Originally from the AFP entry Tarskis_Geometry