traytel [Tue, 18 Feb 2014 14:51:26 +0100] rev 56883
syntactic simplifications of internal (co)datatype constructions
blanchet [Tue, 18 Feb 2014 01:11:25 +0100] rev 56882
follow up of 0819931d652d -- put right induction rule in the old data structure, repairs 'HOL-Proof'-based sessions
blanchet [Mon, 17 Feb 2014 22:54:38 +0100] rev 56881
simplified data structure by reducing the incidence of clumsy indices
blanchet [Mon, 17 Feb 2014 18:18:27 +0100] rev 56880
tuning
* * *
moved 'primrec' up to displace the few remaining uses of 'old_primrec'
wenzelm [Mon, 17 Feb 2014 14:59:09 +0100] rev 56879
made SML/NJ happy;
wenzelm [Mon, 17 Feb 2014 14:07:26 +0100] rev 56878
NEWS;
blanchet [Mon, 17 Feb 2014 13:31:42 +0100] rev 56877
name derivations in 'primrec' for code extraction from proof terms
blanchet [Mon, 17 Feb 2014 13:31:42 +0100] rev 56876
renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)
blanchet [Mon, 17 Feb 2014 13:31:42 +0100] rev 56875
updated NEWS
blanchet [Mon, 17 Feb 2014 13:31:42 +0100] rev 56874
updated keywords