changeset 58878 | f962e42e324d |
parent 58810 | 922a233805d2 |
child 59582 | 0fbed69ff081 |
--- a/src/HOL/NSA/NSA.thy Sun Nov 02 17:09:04 2014 +0100 +++ b/src/HOL/NSA/NSA.thy Sun Nov 02 17:13:28 2014 +0100 @@ -3,7 +3,7 @@ Author: Lawrence C Paulson, University of Cambridge *) -header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*} +section{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*} theory NSA imports HyperDef "~~/src/HOL/Library/Lub_Glb"