# HG changeset patch
# User bauerg
# Date 962871050 -7200
# Node ID ea5b59af6b31196c13b8f7157e753865a7d6598f
# Parent  f9a6670427fb352f0a2f260e6d8350033c8367fe
added;

diff -r f9a6670427fb -r ea5b59af6b31 src/HOL/Real/HahnBanach/HahnBanachLemmas.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/HahnBanachLemmas.thy	Thu Jul 06 10:10:50 2000 +0200
@@ -0,0 +1,3 @@
+
+theory HahnBanachLemmas = HahnBanachSupLemmas + HahnBanachExtLemmas:;
+end;