# HG changeset patch # User nipkow # Date 1122735055 -7200 # Node ID 32626fb8ae495a09d06841805d75992bfd52c567 # Parent f99dd1274c5fa4f511115bc14dcbc8a2860af640 addedd ID line diff -r f99dd1274c5f -r 32626fb8ae49 src/HOL/Hyperreal/Ln.thy --- 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 *}