8 months ago wenzelm [Mon, 27 Nov 2017 15:10:50 +0100] rev 67099
updated to official release of polyml-5.7.1;
back to more modest default heap: e.g. relevant for Pure session for ML IDE;
more robust POLYML_EXE;
Admin/components/components.sha1 Admin/components/main Admin/polyml/README Admin/polyml/settings NEWS lib/scripts/getsettings

8 months ago wenzelm [Mon, 27 Nov 2017 16:07:49 +0100] rev 67098
suppress warning;
src/Pure/Tools/build.scala

8 months ago wenzelm [Mon, 27 Nov 2017 15:59:24 +0100] rev 67097
retain files in Pure.thy, notably $POLYML_EXE;
src/Pure/Thy/sessions.scala

8 months ago wenzelm [Mon, 27 Nov 2017 11:45:20 +0100] rev 67096
proper context (as in 'term' command);
src/HOL/ex/Commands.thy

8 months ago wenzelm [Mon, 27 Nov 2017 11:40:41 +0100] rev 67095
proper treatment of multi-line cartouche as rudiment of antiquotation, e.g. relevant for syntax-highlighting in Isabelle/jEdit;
src/Pure/ML/ml_lex.scala

8 months ago wenzelm [Mon, 27 Nov 2017 10:36:43 +0100] rev 67094
more symbols;
src/HOL/Tools/rewrite_hol_proof.ML

8 months ago wenzelm [Mon, 27 Nov 2017 10:21:52 +0100] rev 67093
prefer Input.source (via cartouche);
src/HOL/Tools/rewrite_hol_proof.ML

8 months ago wenzelm [Mon, 27 Nov 2017 10:04:17 +0100] rev 67092
updated documentation: JVM is always 64bit;
src/Doc/JEdit/JEdit.thy

8 months ago wenzelm [Sun, 26 Nov 2017 21:08:32 +0100] rev 67091
more symbols;
src/HOL/Algebra/AbelCoset.thy src/HOL/Algebra/Bij.thy src/HOL/Algebra/Complete_Lattice.thy src/HOL/Algebra/Congruence.thy src/HOL/Algebra/Coset.thy src/HOL/Algebra/FiniteProduct.thy src/HOL/Algebra/Group.thy src/HOL/Algebra/IntRing.thy src/HOL/Algebra/Lattice.thy src/HOL/Algebra/Order.thy src/HOL/Algebra/Ring.thy src/HOL/Algebra/UnivPoly.thy src/HOL/BNF_Cardinal_Order_Relation.thy src/HOL/BNF_Composition.thy src/HOL/BNF_Def.thy src/HOL/BNF_Fixpoint_Base.thy src/HOL/BNF_Greatest_Fixpoint.thy src/HOL/BNF_Least_Fixpoint.thy src/HOL/BNF_Wellorder_Constructions.thy src/HOL/BNF_Wellorder_Embedding.thy src/HOL/Basic_BNFs.thy src/HOL/Computational_Algebra/Polynomial.thy src/HOL/Computational_Algebra/Primes.thy src/HOL/Conditionally_Complete_Lattices.thy src/HOL/Divides.thy src/HOL/Enum.thy src/HOL/Fields.thy src/HOL/Groebner_Basis.thy src/HOL/HOL.thy src/HOL/Library/BNF_Corec.thy src/HOL/Library/Cardinality.thy src/HOL/Library/DAList.thy src/HOL/Library/Diagonal_Subsequence.thy src/HOL/Library/Extended.thy src/HOL/Library/Extended_Nat.thy src/HOL/Library/Extended_Real.thy src/HOL/Library/FSet.thy src/HOL/Library/Old_Datatype.thy src/HOL/Library/Old_Recdef.thy src/HOL/Library/Option_ord.thy src/HOL/Library/Predicate_Compile_Alternative_Defs.thy src/HOL/Library/Product_Order.thy src/HOL/Library/RBT_Set.thy src/HOL/Library/Ramsey.thy src/HOL/Library/Stream.thy src/HOL/Library/Sublist.thy src/HOL/Library/Sum_of_Squares/sum_of_squares.ML src/HOL/Library/While_Combinator.thy src/HOL/Library/positivstellensatz.ML src/HOL/Limited_Sequence.thy ...

8 months ago wenzelm [Sun, 26 Nov 2017 13:19:52 +0100] rev 67090
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
src/Pure/Isar/keyword.scala