Tue, 12 Nov 2013 13:47:24 +0100export useful ML function
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 55772
export useful ML function

Tue, 12 Nov 2013 13:47:24 +0100moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 55771
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it

Tue, 12 Nov 2013 13:47:24 +0100tuned headers
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 55770
tuned headers

Tue, 12 Nov 2013 13:47:24 +0100moved 'Ctr_Sugar' files out of BNF, so that it can become a general-purpose abstraction
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 55769
moved 'Ctr_Sugar' files out of BNF, so that it can become a general-purpose abstraction

Tue, 12 Nov 2013 12:04:17 +0100updated sessions;
wenzelm [Tue, 12 Nov 2013 12:04:17 +0100] rev 55768
updated sessions;

Tue, 12 Nov 2013 11:52:42 +0100proper latex -- NB: cannot use antiquotation here;
wenzelm [Tue, 12 Nov 2013 11:52:42 +0100] rev 55767
proper latex -- NB: cannot use antiquotation here;

Mon, 11 Nov 2013 22:00:57 +0100merged
wenzelm [Mon, 11 Nov 2013 22:00:57 +0100] rev 55766
merged

Mon, 11 Nov 2013 21:28:08 +0100simplified App template;
wenzelm [Mon, 11 Nov 2013 21:28:08 +0100] rev 55765
simplified App template;

Mon, 11 Nov 2013 21:20:51 +0100obsolete;
wenzelm [Mon, 11 Nov 2013 21:20:51 +0100] rev 55764
obsolete;

Mon, 11 Nov 2013 21:16:23 +0100obsolete;
wenzelm [Mon, 11 Nov 2013 21:16:23 +0100] rev 55763
obsolete;