vdash

Self nominations for Editor: International Journal of Mathematics & Statistics --------------

1 POSTDOC and 1 PHD POSITION in the MathWiki project at Radboud University Nijmegen (NL) http://www.

> How I should prove "1 + 1 = 2" theorem? > Look at Arith.thy in the standard library

You want something like this: theory embedding imports Nat_ZF begin locale embedding = fixes big and

This is the definition of ordered pair in ZF.thy: (* this "symmetric" definition works

Indeed, it looks like SOME is not supported in Isabelle/ZF. You may want to make sure by asking on

> > I want something similar to "obtain" but in definitions (outside of proofs). If

> Does Proof General works with structured Isar proofs Yes.

I sent the previous message too early. The example should look like this: theory example imports

> Is it possible to define new datatypes in Isabelle/ZF? Will it work smoothly? It is possible,

Call for Papers: International Journal of Mathematics and Computation (IJMC). International Journal

Hi! I'm a MSc of Logic student there at the ILLC in Amsterdam. I'm also here because of

Hi Cameron, This sounds great. I live on the West Coast. Is there any chance that this will be video

On Tue, 30 Sep 2008, Ulrik Buchholtz wrote: > Can people start contributing code to the backend,

Hi Marty, The point is that if a system can do formal substitution and navigate up and down a level

> My current thinking on wikis for repositories of formalisations is that wikis can be great for

> Does it make sense to do this over PGIP (like the Isabelle > server > to which you linked)

On Fri, 10 Oct 2008, geu...@gmail.com wrote: > > A very interesting project vdash! > A very

> (2) I haven't seen any really foundational category theory. Is there > any? Category

Hi there, There's another wiki system being developed with similar intent: http://www.kwarc.info/