Re: [Isarmathlib-devel] Direct product

[Sanghyeon Seo]

2008/6/8 Slawomir Kolodynski <address@hidden>:
> I have uploaded DirectProduct_ZF to
> http://formalmath.tiddlyspot.com/#DirectProduct_ZF.
> I have made a couple of changes - see the attached
> file. Here are my comments:

Thanks!

> "constdefs" and "prems" are obsolete in Isabelle 2007.
> I replaced them with "definition" and "assms".

Are they equivalent? If not, what are their differences?

> There is no need to label definitions. Theorems with
> names ending with "_def" corresponding to definitions
> are created automatically by Isabelle.

I know, but is it possible to attach attributes (like [simp])
without using the label?

> {<x,y> \<in> X\<times>Y. y = E(x)}
> {<x,E(x)>.  x\<in>X}
>
> The second way is shorter and I think easier to
> understand.

Agreed. You could put that in the style guide or something.

> I replaced all "<" and ">" characters in the ordered
> pair notation with "\<langle> and "\<rangle>". This
> looks better in the Isabelle generated proof documents
> and my tool for converting IsarMathLib theories to
> TiddlyWiki markup can not handle the "<x,y>" notation
> (and it would be quite difficult to add this feature).

This too, belongs to the style guide.

Where can I find your tool for converting Isabelle theories
to TiddlyWiki markup?

-- 
Seo Sanghyeon