src/HOL/Limits.thy
changeset 52265 bb907eba5902
parent 51642 400ec5ae7f8f
child 53381 355a4cac5440
     1.1 --- a/src/HOL/Limits.thy	Thu May 30 22:30:38 2013 +0200
     1.2 +++ b/src/HOL/Limits.thy	Thu May 30 23:29:33 2013 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      Limits.thy
     1.5 +(*  Title:      HOL/Limits.thy
     1.6      Author:     Brian Huffman
     1.7      Author:     Jacques D. Fleuriot, University of Cambridge
     1.8      Author:     Lawrence C Paulson