wenzelm [Fri, 05 Jun 2015 13:41:06 +0200] rev 60371
added Isar command 'supply';
wenzelm [Fri, 05 Jun 2015 13:26:12 +0200] rev 60370
tuned;
wenzelm [Fri, 05 Jun 2015 11:11:26 +0200] rev 60369
clarified signature -- better support for Isar commands outside of Pure;
wenzelm [Wed, 03 Jun 2015 21:48:40 +0200] rev 60368
merged
wenzelm [Wed, 03 Jun 2015 19:25:05 +0200] rev 60367
clarified context;
wenzelm [Tue, 02 Jun 2015 23:00:50 +0200] rev 60366
tuned;
wenzelm [Tue, 02 Jun 2015 19:56:29 +0200] rev 60365
clarified context;
wenzelm [Tue, 02 Jun 2015 17:27:01 +0200] rev 60364
cleaified context;
more uniform context data;
tuned;
wenzelm [Tue, 02 Jun 2015 13:55:43 +0200] rev 60363
clarified context;
wenzelm [Tue, 02 Jun 2015 11:03:02 +0200] rev 60362
clarified context;
wenzelm [Tue, 02 Jun 2015 10:12:46 +0200] rev 60361
clarified context;
wenzelm [Tue, 02 Jun 2015 10:12:29 +0200] rev 60360
clarified context;
wenzelm [Tue, 02 Jun 2015 09:40:04 +0200] rev 60359
clarified context;
wenzelm [Tue, 02 Jun 2015 09:16:19 +0200] rev 60358
clarified context;
wenzelm [Tue, 02 Jun 2015 09:10:05 +0200] rev 60357
tuned proof;
noschinl [Wed, 03 Jun 2015 09:32:49 +0200] rev 60356
merged
noschinl [Tue, 02 Jun 2015 13:14:36 +0200] rev 60355
simps_of_case: Better error if split rule is not an equality
noschinl [Tue, 02 Jun 2015 13:14:11 +0200] rev 60354
simps_of_case: allow Drule.dummy_thm as ignored split rule
haftmann [Mon, 01 Jun 2015 18:59:22 +0200] rev 60353
implicit partial divison operation in integral domains
haftmann [Mon, 01 Jun 2015 18:59:21 +0200] rev 60352
separate class for division operator, with particular syntax added in more specific classes
haftmann [Mon, 01 Jun 2015 18:59:21 +0200] rev 60351
explicit check for field sort, to anticipate situation where syntactic checking alone will not be sufficient any longer
haftmann [Mon, 01 Jun 2015 18:59:21 +0200] rev 60350
dropped dead config option
haftmann [Mon, 01 Jun 2015 18:59:20 +0200] rev 60349
tuned, including proper signature for functor argument
haftmann [Mon, 01 Jun 2015 18:59:20 +0200] rev 60348
dropped dead code
haftmann [Mon, 01 Jun 2015 18:59:20 +0200] rev 60347
explicit argument expansion of uncheck rules;
rewriting of user-space type system must behave similarly to abbreviations
haftmann [Mon, 01 Jun 2015 18:59:20 +0200] rev 60346
explicit input marker for operations
haftmann [Mon, 01 Jun 2015 18:59:20 +0200] rev 60345
completely separated canonical class abbreviations from abbreviations stemming from non-canonical morphisms -- these have no shared concept
haftmann [Mon, 01 Jun 2015 18:59:20 +0200] rev 60344
self-contained formulation of abbrev for named targets