--- a/src/HOL/Hyperreal/Ln.thy Fri Jul 29 19:47:41 2005 +0200 +++ b/src/HOL/Hyperreal/Ln.thy Sat Jul 30 16:50:55 2005 +0200 @@ -1,5 +1,6 @@ (* Title: Ln.thy Author: Jeremy Avigad + ID: $Id$ *) header {* Properties of ln *}