2005-10-25 ago avoid legacy goals;
2005-10-21 ago Goal.prove;
2005-09-16 ago use mem operator
2005-09-15 ago merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
2005-09-12 ago add header
2005-09-12 ago added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
2005-09-12 ago new implementation of transfer principle