haftmann [Thu, 13 Mar 2014 08:56:08 +0100] rev 56077
tuned proofs
haftmann [Thu, 13 Mar 2014 08:56:08 +0100] rev 56076
dropped redundant theorems
haftmann [Thu, 13 Mar 2014 08:56:08 +0100] rev 56075
tuned
haftmann [Thu, 13 Mar 2014 08:56:07 +0100] rev 56074
monotonicity in complete lattices
nipkow [Thu, 13 Mar 2014 07:07:07 +0100] rev 56073
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
wenzelm [Wed, 12 Mar 2014 22:57:50 +0100] rev 56072
tuned signature -- clarified module name;
wenzelm [Wed, 12 Mar 2014 22:44:55 +0100] rev 56071
added ML antiquotation @{here};
wenzelm [Wed, 12 Mar 2014 22:41:04 +0100] rev 56070
ML_Context.check_antiquotation still required;
wenzelm [Wed, 12 Mar 2014 21:58:48 +0100] rev 56069
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
added command 'print_ML_antiquotations';
wenzelm [Wed, 12 Mar 2014 21:29:46 +0100] rev 56068
proper base comparison;