Mercurial Mercurial > wneuper > isa / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | bz2 | gz | help
fixed import: requires ContNotDenum;
authorwenzelm
Wed, 10 Dec 2008 23:13:21 +0100
changeset 29043409d1ca929b5
parent 29042 d5a5888b8c54
child 29044 45dfd04a972e
fixed import: requires ContNotDenum;
src/HOL/Real/HahnBanach/Bounds.thy file | annotate | diff | comparison | revisions 
     1.1 --- a/src/HOL/Real/HahnBanach/Bounds.thy	Wed Dec 10 22:46:42 2008 +0100
     1.2 +++ b/src/HOL/Real/HahnBanach/Bounds.thy	Wed Dec 10 23:13:21 2008 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Bounds *}
     1.5  
     1.6  theory Bounds
     1.7 -imports Main Real
     1.8 +imports Main ContNotDenum
     1.9  begin
    1.10  
    1.11  locale lub =
wneuper/isa