src/HOL/Library/Polynomial_Factorial.thy
changeset 63764 f3ad26c4b2d9
parent 63722 b9c8da46443b
child 63830 2ea3725a34bd
     1.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Thu Sep 01 21:28:46 2016 +0200
     1.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Thu Sep 01 21:28:55 2016 +0200
     1.3 @@ -1,3 +1,11 @@
     1.4 +(*  Title:      HOL/Library/Polynomial_Factorial.thy
     1.5 +    Author:     Brian Huffman
     1.6 +    Author:     Clemens Ballarin
     1.7 +    Author:     Amine Chaieb
     1.8 +    Author:     Florian Haftmann
     1.9 +    Author:     Manuel Eberl
    1.10 +*)
    1.11 +
    1.12  theory Polynomial_Factorial
    1.13  imports 
    1.14    Complex_Main
    1.15 @@ -1470,4 +1478,4 @@
    1.16    
    1.17  value [code] "Lcm {[:1,2,3:], [:2,3,4::int poly:]}"
    1.18  
    1.19 -end
    1.20 \ No newline at end of file
    1.21 +end