isabelle: Changelog

wenzelm [Thu, 01 Feb 2018 20:29:53 +0100] rev 67565

tuned: more standard use of order;

wenzelm [Thu, 01 Feb 2018 17:27:13 +0100] rev 67564

tuned;

wenzelm [Thu, 01 Feb 2018 17:21:58 +0100] rev 67563

tuned;

wenzelm [Thu, 01 Feb 2018 17:15:07 +0100] rev 67562

clarified signature; eliminated aliases of Thm.term_ord;

wenzelm [Thu, 01 Feb 2018 15:31:25 +0100] rev 67561

clarified signature: prefer proper order operation;

wenzelm [Thu, 01 Feb 2018 15:12:57 +0100] rev 67560

tuned signature: more operations;

wenzelm [Thu, 01 Feb 2018 13:55:10 +0100] rev 67559

clarified signature;

wenzelm [Wed, 31 Jan 2018 21:05:47 +0100] rev 67558

proper term_ord as in HOL/Library/positivstellensatz.ML, e.g. relevant for "0 <= c & 0 <= a ==> a + bb = 1 & c <= 1 ==> bb * c * 4 <= (12::real)";

wenzelm [Wed, 31 Jan 2018 14:20:39 +0100] rev 67557

performance fine-tuning of hot spot;

wenzelm [Wed, 31 Jan 2018 14:11:57 +0100] rev 67556

tuned;

isabelle