changeset 55715 | c4159fe6fa46 |
parent 55682 | b1d955791529 |
child 55862 | 03ff4d1e6784 |
1.1 --- a/src/HOL/NSA/NSA.thy Tue Nov 05 09:45:00 2013 +0100 1.2 +++ b/src/HOL/NSA/NSA.thy Tue Nov 05 09:45:02 2013 +0100 1.3 @@ -6,7 +6,7 @@ 1.4 header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*} 1.5 1.6 theory NSA 1.7 -imports HyperDef 1.8 +imports HyperDef "~~/src/HOL/Library/Lubs_Glbs" 1.9 begin 1.10 1.11 definition