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
haftmann [Mon, 01 Jun 2015 18:59:20 +0200] rev 60343
correct sort constraints for abbreviations in type classes
* * *
yet another bunch of corrections
haftmann [Mon, 01 Jun 2015 18:59:20 +0200] rev 60342
separate function to compute exported abbreviation
haftmann [Mon, 01 Jun 2015 18:59:20 +0200] rev 60341
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann [Mon, 01 Jun 2015 18:59:20 +0200] rev 60340
tuned order
haftmann [Mon, 01 Jun 2015 18:59:20 +0200] rev 60339
dedicated config options to deactivate uncheck phase for improvable syntax
haftmann [Mon, 01 Jun 2015 18:59:19 +0200] rev 60338
clarified interfaces for improvable syntax
haftmann [Mon, 01 Jun 2015 18:59:19 +0200] rev 60337
tuned
wenzelm [Mon, 01 Jun 2015 18:07:36 +0200] rev 60336
clarified context;
wenzelm [Mon, 01 Jun 2015 17:44:45 +0200] rev 60335
clarified context;
wenzelm [Mon, 01 Jun 2015 17:08:47 +0200] rev 60334
clarified context;
wenzelm [Mon, 01 Jun 2015 16:07:38 +0200] rev 60333
tuned;
wenzelm [Mon, 01 Jun 2015 15:39:53 +0200] rev 60332
discontinued unused / unmaintained SVC oracle -- current Isabelle tools (e.g. arith, smt) can easily solve the given examples with full proof reconstruction;
wenzelm [Mon, 01 Jun 2015 15:06:09 +0200] rev 60331
discontinued legacy;
wenzelm [Mon, 01 Jun 2015 13:52:35 +0200] rev 60330
obsolete (see 189c81779a68);
wenzelm [Mon, 01 Jun 2015 13:46:23 +0200] rev 60329
eliminated odd C combinator -- Isabelle/ML usually has canonical argument order;
wenzelm [Mon, 01 Jun 2015 13:35:16 +0200] rev 60328
clarified context;
wenzelm [Mon, 01 Jun 2015 13:32:36 +0200] rev 60327
clarified context;
wenzelm [Mon, 01 Jun 2015 11:47:25 +0200] rev 60326
tuned;
wenzelm [Mon, 01 Jun 2015 11:46:03 +0200] rev 60325
clarified context;
wenzelm [Mon, 01 Jun 2015 10:47:08 +0200] rev 60324
tuned;
wenzelm [Sun, 31 May 2015 00:20:35 +0200] rev 60323
obsolete;
wenzelm [Sun, 31 May 2015 00:17:47 +0200] rev 60322
clarified context;
wenzelm [Sun, 31 May 2015 00:16:26 +0200] rev 60321
tuned;
wenzelm [Sun, 31 May 2015 00:11:12 +0200] rev 60320
tuned;
wenzelm [Sat, 30 May 2015 23:58:06 +0200] rev 60319
standardize towards Thm.eta_long_conversion, which just does eta_long conversion;
wenzelm [Sat, 30 May 2015 23:30:54 +0200] rev 60318
tuned spelling;