blanchet [Thu, 13 Mar 2014 13:18:13 +0100] rev 56080
removed tracing output
blanchet [Thu, 13 Mar 2014 13:18:13 +0100] rev 56079
use 'smt2' in SMT examples as much as currently possible
blanchet [Thu, 13 Mar 2014 13:18:13 +0100] rev 56078
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
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;
wenzelm [Wed, 12 Mar 2014 21:28:09 +0100] rev 56067
tuned;
wenzelm [Wed, 12 Mar 2014 17:25:28 +0100] rev 56066
tuned proofs;
wenzelm [Wed, 12 Mar 2014 17:02:05 +0100] rev 56065
more explicit markup and explanation of the improper status of 'back', following the AFP style-guide;