blanchet [Tue, 12 Nov 2013 14:00:56 +0100] rev 54406
undid copy-paste
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 54405
ported 'partial_function' to 'Ctr_Sugar' abstraction
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 54404
port list comprehension simproc to 'Ctr_Sugar' abstraction
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 54403
added convenience function
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 54402
document idiomatic use of 'simps_of_case'
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 54401
ported 'Simps_Case_Conv' to use new 'Ctr_Sugar' abstraction
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 54400
register old-style datatypes as 'Ctr_Sugar'
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 54399
export useful ML function
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 54398
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 54397
tuned headers
blanchet [Tue, 12 Nov 2013 13:47:24 +0100] rev 54396
moved 'Ctr_Sugar' files out of BNF, so that it can become a general-purpose abstraction
wenzelm [Tue, 12 Nov 2013 12:04:17 +0100] rev 54395
updated sessions;
wenzelm [Tue, 12 Nov 2013 11:52:42 +0100] rev 54394
proper latex -- NB: cannot use antiquotation here;
wenzelm [Mon, 11 Nov 2013 22:00:57 +0100] rev 54393
merged
wenzelm [Mon, 11 Nov 2013 21:28:08 +0100] rev 54392
simplified App template;
wenzelm [Mon, 11 Nov 2013 21:20:51 +0100] rev 54391
obsolete;
wenzelm [Mon, 11 Nov 2013 21:16:23 +0100] rev 54390
obsolete;
wenzelm [Mon, 11 Nov 2013 21:04:30 +0100] rev 54389
tuned message;
wenzelm [Mon, 11 Nov 2013 20:50:12 +0100] rev 54388
tuned signature -- removed obsolete Addsimprocs, Delsimprocs;
wenzelm [Mon, 11 Nov 2013 20:00:53 +0100] rev 54387
tuned signature;
blanchet [Mon, 11 Nov 2013 20:51:00 +0100] rev 54386
minor doc fix
wenzelm [Mon, 11 Nov 2013 18:37:56 +0100] rev 54385
merged
wenzelm [Mon, 11 Nov 2013 17:44:21 +0100] rev 54384
merged, using src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML and src/HOL/Tools/Sledgehammer/sledgehammer_run.ML from 347c3b0cab44;
wenzelm [Mon, 11 Nov 2013 17:34:44 +0100] rev 54383
removed obsolete RC tags;