Thu, 09 Nov 2006 23:33:55 +0100 chaieb oracle raises CooperDec.COOPER instead of COOPER (this is eliminated). Erronous old behaviour due to this exception is now correcrted.
Thu, 09 Nov 2006 21:44:35 +0100 wenzelm LocalTheory.restore;
Thu, 09 Nov 2006 21:44:34 +0100 wenzelm init: '-' refers to global context;
Thu, 09 Nov 2006 21:44:33 +0100 wenzelm abbrevs: return result;
Thu, 09 Nov 2006 21:44:32 +0100 wenzelm Stack.map_top;
Thu, 09 Nov 2006 21:44:31 +0100 wenzelm abbrevs: return result;
Thu, 09 Nov 2006 21:44:30 +0100 wenzelm separate map_top/all;
Thu, 09 Nov 2006 21:44:29 +0100 wenzelm abbrevs: return result (use LocalTheory.abbrevs directly);
Thu, 09 Nov 2006 21:44:28 +0100 wenzelm tuned;
Thu, 09 Nov 2006 21:44:27 +0100 wenzelm abbrevs: return result;
Thu, 09 Nov 2006 18:58:52 +0100 webertj timing/tracing code removed
Thu, 09 Nov 2006 18:48:45 +0100 webertj interpreters for fst and snd added
Thu, 09 Nov 2006 16:14:43 +0100 webertj new CCS-based implementation that should work with PolyML 5.0
Thu, 09 Nov 2006 11:58:51 +0100 wenzelm HOL: less/less_eq on bool, modified syntax;
(0) -10000 -3000 -1000 -300 -100 -14 +14 +100 +300 +1000 +3000 +10000 +30000 tip