Notation question

[John Hughes]

	> > >  G |- f :: all x::S . T   G |- s :: S
	> > >--------------------------------------
	> > >          G |- f s :: [s/x]T
	>

	    Any more takers? I still don't have any pointers to literature where 
	this theorem notation is explained more fully, and I'd really like to have 
	some.

This is a standard notation for describing type systems in articles on the
subject -- so standard that it's hard to think of a good reference that
actually explains it! However, I'd suggest looking at Michael Schwartzbach's
lecture notes on Polymorphic Type Inference, which are on the web at

	http://www.daimi.aau.dk/~mis/typeinf.ps

The typing rule notation is explained in the first couple of pages, and then
used to explain many variants on type systems, show how inference works, etc.

I have a collection of links to such articles at

	http://www.md.chalmers.se/~rjmh/tutorials.html

which you might find useful.

John Hughes