> thanks for reporting this. I hope to eliminate this problem within this
> day.
http://isabelle.in.tum.de/repos/isabelle/shortlog
Done
Florian
-- next part --
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 byt
Hi Brian,
thanks for reporting this. I hope to eliminate this problem within this
day.
Hope this helps,
Florian
Brian Huffman schrieb:
> Hi all,
>
> I recently tried to make some changes to the topological_space class
> in RealVector.thy (I moved the definition of "open" here from
> Li
On Mon, Jun 8, 2009 at 12:20 AM, Florian
Haftmann wrote:
>> thanks for reporting this. ?I hope to eliminate this problem within this
>> day.
>
> http://isabelle.in.tum.de/repos/isabelle/shortlog
>
> Done
> ? ? ? ?Florian
It works - thanks!
- Brian
Hi all,
I recently tried to make some changes to the topological_space class
in RealVector.thy (I moved the definition of "open" here from
Library/Topology_Euclidean_Space.thy). Here is the declaration of the
syntactic class for the "open" predicate:
class "open" = fixes "open" :: "'a set => bool
