User Details
User Details
- User Since
- Sep 24 2019, 9:33 PM (192 w, 2 d)
- Roles
- Administrator
Wed, May 31
Wed, May 31
provide scala-3.3.0;
makarius committed rISABELLE163e4835a8db: enable scala-3.3.0, with forced rebuild of Isabelle/Scala and Isabelle/ML;.
enable scala-3.3.0, with forced rebuild of Isabelle/Scala and Isabelle/ML;
Tue, May 30
Tue, May 30
Sat, May 27
Sat, May 27
clarified treatment of context;
clarified treatment of context;
Thu, May 25
Thu, May 25
prefer @{attributes} antiquotation over Attrib.internal;
makarius committed rISABELLE2cd7e5518d0d: clarified output of embedded values, e.g. for 'print_locale';.
clarified output of embedded values, e.g. for 'print_locale';
makarius committed rISABELLE4d9349989d94: more uniform simproc_setup: avoid vacuous abstraction over morphism, which….
more uniform simproc_setup: avoid vacuous abstraction over morphism, which…
proper setup for rule attribute;
tuned: more antiquotations;
tuned signature: more position information;
Mon, May 22
Mon, May 22
adapted to current Isabelle/ec1c0daa3fbd;
adapted to Isabelle/5edd5b12017d;
adapted to current Isabelle/ec1c0daa3fbd;
backout a8e9b33d75e1, thanks to Isabelle/f0aca0506531;
proper morphism context;
makarius added a reverting change for rAFPa8e9b33d75e1: adapted to Isabelle/5ab5add88922;: rAFP88780e621a30: backout a8e9b33d75e1, thanks to Isabelle/f0aca0506531;.
proper morphism context;
adapted to Isabelle/5ab5add88922;
misc tuning and clarification;
makarius committed rISABELLE3fde7a52c650: tuned --- Token.make_string / Token.assign are value-oriented;.
tuned --- Token.make_string / Token.assign are value-oriented;
more documentation;
makarius committed rISABELLEf0aca0506531: more robust context: fail immediately via Morphism.the_theory, instead of….
more robust context: fail immediately via Morphism.the_theory, instead of…
prefer static simpset;
omit pointless morphism in global theory;
more careful treatment of context for method source;
more careful reset_context for stored entity;
remove pointless context setup (see also b2e449c155a4);
clarified signature;
more careful reset/set_context for stored declarations;
clarified data: avoid pointless Morphism.transform;
clarified signature: more explicit types;
proper Token.Declaration for internal_declaration;
more standard treatment of morphism context;
tuned: avoid duplication;
makarius committed rISABELLEa71bfc551891: more standard treatment of morphism context, but hardly relevant here;.
more standard treatment of morphism context, but hardly relevant here;
makarius committed rISABELLE11d6a1e62841: more careful treatment of set_context / reset_context for persistent morphisms;.
more careful treatment of set_context / reset_context for persistent morphisms;
makarius committed rISABELLE4e865c45458b: clarified transfer / trim_context on persistent Token.source (e.g. attribute….
clarified transfer / trim_context on persistent Token.source (e.g. attribute…
makarius committed rISABELLE5ab5add88922: proper transfer to supported "bundle ... begin unbundle ... end", e.g. see….
proper transfer to supported "bundle ... begin unbundle ... end", e.g. see…
makarius committed rISABELLEedb195122938: support for context within morphism (for background theory);.
support for context within morphism (for background theory);
clarified signature;
clarified stored thm: result from notes;
more accurate Thm.trim_context / Thm.transfer;
makarius committed rISABELLE0912b519c5db: update to polyml-a5d5fba90286, with more robust ML_Heap.sizeof;.
update to polyml-a5d5fba90286, with more robust ML_Heap.sizeof;
clarified signature: avoid convoluted operations;
makarius committed rISABELLEf16067da45ef: avoid capture of inner/outer context and thus reduce heaps sizes by 20..40%….
avoid capture of inner/outer context and thus reduce heaps sizes by 20..40%…
proper transfer / trim_context;
makarius committed rISABELLEec817f4486b3: more operations "without_context", assuming that the thm has been properly….
more operations "without_context", assuming that the thm has been properly…
tuned: more accurate check (is_norm_hhf protect);
proper trim_context / transfer;
makarius committed rISABELLE2c3f4d80abfb: more standard merge order, following logical structure of imports rather than….
more standard merge order, following logical structure of imports rather than…
clarified build options: reduce heap size by approx. 3%;
proper Thm.trim_context / Thm.transfer;
makarius committed rISABELLE9da707dad2a3: tuned: avoid pointless Proof_Context.init_global of Context.proof_of;.
tuned: avoid pointless Proof_Context.init_global of Context.proof_of;
proper Thm.trim_context / Thm.transfer;
Fri, May 12
Fri, May 12
proper Thm.trim_context / Thm.transfer;
proper position for ML-like commands;
adapted to Isabelle/f78cdc6fe971;
adapted to Isabelle/f78cdc6fe971;
Thu, May 11
Thu, May 11
more robust: after shutdown;
proper exception CONTEXT for Context.certificate_theory;
more diagnostic operations;
more standard treatment of data and context;
more standard val silent = Attrib.setup_config_bool;
adapted to 3f354d5bbf98;
Wed, May 10
Wed, May 10
proper Thm.trim_context / Thm.transfer;