src/HOL/Hyperreal/StarDef.thy
2006-01-19 ago setup: theory -> theory;
2005-09-17 ago use interpretation command
2005-09-15 ago merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up