16 months ago wenzelm [Thu, 01 Feb 2018 15:12:57 +0100] rev 67560
tuned signature: more operations;
src/HOL/Algebra/ringsimp.ML src/HOL/Analysis/normarith.ML src/HOL/Library/Sum_of_Squares/sum_of_squares.ML src/HOL/Library/positivstellensatz.ML src/HOL/Tools/ATP/atp_systems.ML src/HOL/Tools/Nitpick/kodkod.ML src/HOL/Tools/Nitpick/kodkod_sat.ML src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML src/HOL/Tools/numeral_simprocs.ML src/HOL/Tools/semiring_normalizer.ML src/Pure/library.ML src/Tools/Argo/argo_heap.ML src/Tools/Argo/argo_simplex.ML src/Tools/float.ML

16 months ago wenzelm [Thu, 01 Feb 2018 13:55:10 +0100] rev 67559
clarified signature;
src/HOL/Analysis/normarith.ML src/HOL/Decision_Procs/langford.ML src/HOL/Library/Sum_of_Squares/sum_of_squares.ML src/HOL/Library/positivstellensatz.ML src/HOL/Tools/Qelim/cooper.ML src/HOL/Tools/groebner.ML src/HOL/Tools/sat.ML src/HOL/Tools/semiring_normalizer.ML src/Pure/Isar/rule_cases.ML src/Pure/more_thm.ML

16 months ago 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)";
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML

16 months ago wenzelm [Wed, 31 Jan 2018 14:20:39 +0100] rev 67557
performance fine-tuning of hot spot;
src/Pure/General/table.ML

16 months ago wenzelm [Wed, 31 Jan 2018 14:11:57 +0100] rev 67556
tuned;
src/Pure/Syntax/lexicon.ML src/Pure/Syntax/parser.ML

16 months ago wenzelm [Wed, 31 Jan 2018 14:02:37 +0100] rev 67555
more efficient tokens_match_ord based on token_kind_index;
tuned;
src/Pure/Syntax/lexicon.ML

16 months ago wenzelm [Wed, 31 Jan 2018 11:49:56 +0100] rev 67554
more abstract type;
src/Pure/Syntax/lexicon.ML

16 months ago wenzelm [Wed, 31 Jan 2018 11:46:55 +0100] rev 67553
tuned;
src/Pure/Syntax/simple_syntax.ML

16 months ago wenzelm [Wed, 31 Jan 2018 11:40:26 +0100] rev 67552
clarified signature;
src/Pure/Syntax/lexicon.ML src/Pure/Syntax/parser.ML src/Pure/Syntax/simple_syntax.ML

16 months ago wenzelm [Wed, 31 Jan 2018 11:26:50 +0100] rev 67551
clarified signature;
src/Pure/Syntax/lexicon.ML src/Pure/Syntax/parser.ML