Page MenuHomeIsabelle/Phabricator

makarius (Makarius Wenzel)
UserAdministrator

Projects

User Details

User Since
Sep 24 2019, 9:33 PM (192 w, 2 d)
Roles
Administrator

Recent Activity

Wed, May 31

makarius committed rISABELLE96e2c2bbacbd: provide scala-3.3.0;.
provide scala-3.3.0;
Wed, May 31, 11:41 AM
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;
Wed, May 31, 11:41 AM
makarius committed rISABELLE26b31f402948: tuned NEWS;.
tuned NEWS;
Wed, May 31, 11:41 AM
makarius committed rISABELLE9609085da969: more NEWS;.
more NEWS;
Wed, May 31, 11:41 AM

Tue, May 30

makarius created Blog Post: Significantly reduced ML heap usage.
Tue, May 30, 12:18 PM
makarius committed rISABELLEf3d19c8445ec: NEWS;.
NEWS;
Tue, May 30, 12:08 PM

Sat, May 27

makarius committed rISABELLEcc17e2f0f1fc: merged.
merged
Sat, May 27, 7:11 PM
makarius committed rISABELLEf360ee6ce670: tuned signature;.
tuned signature;
Sat, May 27, 7:11 PM
makarius committed rISABELLE43154a48da69: clarified treatment of context;.
clarified treatment of context;
Sat, May 27, 7:11 PM
makarius committed rISABELLEb14421dc6759: clarified treatment of context;.
clarified treatment of context;
Sat, May 27, 7:11 PM
makarius committed rISABELLE10487f6571bc: more operations;.
more operations;
Sat, May 27, 7:11 PM

Thu, May 25

makarius committed rAFPae5dec7716f4: prefer @{attributes} antiquotation over Attrib.internal;.
prefer @{attributes} antiquotation over Attrib.internal;
Thu, May 25, 8:21 PM
makarius committed rAFP91c7c75dea9e: merged.
merged
Thu, May 25, 8:21 PM
makarius committed rAFPa023f98be016: tuned proofs;.
tuned proofs;
Thu, May 25, 8:21 PM
makarius committed rISABELLE300537844bb7: merged.
merged
Thu, May 25, 8:18 PM
makarius committed rISABELLE2cd7e5518d0d: clarified output of embedded values, e.g. for 'print_locale';.
clarified output of embedded values, e.g. for 'print_locale';
Thu, May 25, 8:18 PM
makarius committed rISABELLE4d9349989d94: more uniform simproc_setup: avoid vacuous abstraction over morphism, which….
more uniform simproc_setup: avoid vacuous abstraction over morphism, which…
Thu, May 25, 8:18 PM
makarius committed rISABELLE35439ca0133c: proper setup for rule attribute;.
proper setup for rule attribute;
Thu, May 25, 8:18 PM
makarius committed rISABELLE838198d17a40: tuned;.
tuned;
Thu, May 25, 8:18 PM
makarius committed rISABELLE2ea20bb1493c: tuned: more antiquotations;.
tuned: more antiquotations;
Thu, May 25, 8:18 PM
makarius committed rISABELLEbc42c074e58f: tuned signature: more position information;.
tuned signature: more position information;
Thu, May 25, 8:18 PM
makarius committed rISABELLEc3efa0b63d2e: tuned;.
tuned;
Thu, May 25, 8:18 PM

Mon, May 22

makarius committed rAFPe74d656c954e: merged.
merged
Mon, May 22, 8:21 PM
makarius committed rAFPbfdfdc4ec622: merged.
merged
Mon, May 22, 8:21 PM
makarius committed rAFP56196e009aa3: adapted to current Isabelle/ec1c0daa3fbd;.
adapted to current Isabelle/ec1c0daa3fbd;
Mon, May 22, 8:21 PM
makarius committed rAFP5aeaa920938a: adapted to Isabelle/5edd5b12017d;.
adapted to Isabelle/5edd5b12017d;
Mon, May 22, 8:21 PM
makarius committed rAFPd057ea280883: adapted to current Isabelle/ec1c0daa3fbd;.
adapted to current Isabelle/ec1c0daa3fbd;
Mon, May 22, 8:21 PM
makarius committed rAFP88780e621a30: backout a8e9b33d75e1, thanks to Isabelle/f0aca0506531;.
backout a8e9b33d75e1, thanks to Isabelle/f0aca0506531;
Mon, May 22, 8:21 PM
makarius committed rAFP34d24aa19ac7: proper morphism context;.
proper morphism context;
Mon, May 22, 8:21 PM
makarius added a reverting change for rAFPa8e9b33d75e1: adapted to Isabelle/5ab5add88922;: rAFP88780e621a30: backout a8e9b33d75e1, thanks to Isabelle/f0aca0506531;.
Mon, May 22, 8:21 PM
makarius committed rAFP86eda777a3c5: proper morphism context;.
proper morphism context;
Mon, May 22, 8:21 PM
makarius committed rAFPa8e9b33d75e1: adapted to Isabelle/5ab5add88922;.
adapted to Isabelle/5ab5add88922;
Mon, May 22, 8:21 PM
makarius committed rISABELLE070703d83cfe: merged.
merged
Mon, May 22, 8:10 PM
makarius committed rISABELLEec1c0daa3fbd: misc tuning and clarification;.
misc tuning and clarification;
Mon, May 22, 8:10 PM
makarius committed rISABELLE79ad3181071b: tuned signature;.
tuned signature;
Mon, May 22, 8:10 PM
makarius committed rISABELLE52d071212a7a: tuned;.
tuned;
Mon, May 22, 8:10 PM
makarius committed rISABELLE3fde7a52c650: tuned --- Token.make_string / Token.assign are value-oriented;.
tuned --- Token.make_string / Token.assign are value-oriented;
Mon, May 22, 8:10 PM
makarius committed rISABELLEdd7bb7f99ad5: tuned signature;.
tuned signature;
Mon, May 22, 8:10 PM
makarius committed rISABELLE5edd5b12017d: tuned signature;.
tuned signature;
Mon, May 22, 8:10 PM
makarius committed rISABELLE90b64ffc48a3: more documentation;.
more documentation;
Mon, May 22, 8:10 PM
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…
Mon, May 22, 8:10 PM
makarius committed rISABELLE3357bc875b11: prefer static simpset;.
prefer static simpset;
Mon, May 22, 8:10 PM
makarius committed rISABELLE40db83793cea: more operations;.
more operations;
Mon, May 22, 8:10 PM
makarius committed rISABELLEa51d2e96203e: omit pointless morphism in global theory;.
omit pointless morphism in global theory;
Mon, May 22, 8:10 PM
makarius committed rISABELLEb0bcba8afdd8: more careful treatment of context for method source;.
more careful treatment of context for method source;
Mon, May 22, 8:10 PM
makarius committed rISABELLE270e85124a9a: clarified context;.
clarified context;
Mon, May 22, 8:10 PM
makarius committed rISABELLEb2e449c155a4: more careful reset_context for stored entity;.
more careful reset_context for stored entity;
Mon, May 22, 8:10 PM
makarius committed rISABELLE5c3e8e6f430a: remove pointless context setup (see also b2e449c155a4);.
remove pointless context setup (see also b2e449c155a4);
Mon, May 22, 8:10 PM
makarius committed rISABELLE35a86345de48: clarified signature;.
clarified signature;
Mon, May 22, 8:10 PM
makarius committed rISABELLE073826f50e14: tuned;.
tuned;
Mon, May 22, 8:10 PM
makarius committed rISABELLE15ab73949713: more careful reset/set_context for stored declarations;.
more careful reset/set_context for stored declarations;
Mon, May 22, 8:10 PM
makarius committed rISABELLEb8dfaba8394f: tuned;.
tuned;
Mon, May 22, 8:10 PM
makarius committed rISABELLE61a1bf9eb0ce: clarified data: avoid pointless Morphism.transform;.
clarified data: avoid pointless Morphism.transform;
Mon, May 22, 8:10 PM
makarius committed rISABELLE001739cb8d08: clarified signature: more explicit types;.
clarified signature: more explicit types;
Mon, May 22, 8:10 PM
makarius committed rISABELLEdbc67f6c501c: proper Token.Declaration for internal_declaration;.
proper Token.Declaration for internal_declaration;
Mon, May 22, 8:10 PM
makarius committed rISABELLEe5bd9b3c6f0f: more standard treatment of morphism context;.
more standard treatment of morphism context;
Mon, May 22, 8:10 PM
makarius committed rISABELLEa01c3bcf22dd: tuned: avoid duplication;.
tuned: avoid duplication;
Mon, May 22, 8:10 PM
makarius committed rISABELLEa71bfc551891: more standard treatment of morphism context, but hardly relevant here;.
more standard treatment of morphism context, but hardly relevant here;
Mon, May 22, 8:10 PM
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;
Mon, May 22, 8:10 PM
makarius committed rISABELLEe6343330e8df: tuned;.
tuned;
Mon, May 22, 8:10 PM
makarius committed rISABELLE7c9f290dff55: tuned signature;.
tuned signature;
Mon, May 22, 8:10 PM
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…
Mon, May 22, 8:10 PM
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…
Mon, May 22, 8:10 PM
makarius committed rISABELLEedb195122938: support for context within morphism (for background theory);.
support for context within morphism (for background theory);
Mon, May 22, 8:10 PM
makarius committed rISABELLEb6c886b7184f: clarified signature;.
clarified signature;
Mon, May 22, 8:10 PM
makarius committed rISABELLEd555983054f3: tuned;.
tuned;
Mon, May 22, 8:10 PM
makarius committed rISABELLE2d60172c0ade: clarified stored thm: result from notes;.
clarified stored thm: result from notes;
Mon, May 22, 8:10 PM
makarius committed rISABELLE9439ae944a00: tuned signature;.
tuned signature;
Mon, May 22, 8:10 PM
makarius committed rISABELLE9de0d3d961d4: tuned;.
tuned;
Mon, May 22, 8:10 PM
makarius committed rISABELLE904242f46ce1: more accurate Thm.trim_context / Thm.transfer;.
more accurate Thm.trim_context / Thm.transfer;
Mon, May 22, 8:10 PM
makarius committed rISABELLE92d487a28545: tuned signature;.
tuned signature;
Mon, May 22, 8:10 PM
makarius committed rISABELLEbb60ea7318d6: tuned whitespace;.
tuned whitespace;
Mon, May 22, 8:10 PM
makarius committed rISABELLE0912b519c5db: update to polyml-a5d5fba90286, with more robust ML_Heap.sizeof;.
update to polyml-a5d5fba90286, with more robust ML_Heap.sizeof;
Mon, May 22, 8:10 PM
makarius committed rISABELLE64f81d011a90: clarified signature: avoid convoluted operations;.
clarified signature: avoid convoluted operations;
Mon, May 22, 8:10 PM
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%…
Mon, May 22, 8:10 PM
makarius committed rISABELLEd7395ef81292: proper transfer / trim_context;.
proper transfer / trim_context;
Mon, May 22, 8:10 PM
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…
Mon, May 22, 8:10 PM
makarius committed rISABELLE78deba4fdf27: tuned: more accurate check (is_norm_hhf protect);.
tuned: more accurate check (is_norm_hhf protect);
Mon, May 22, 8:10 PM
makarius committed rISABELLEc8c084bd7e12: proper trim_context / transfer;.
proper trim_context / transfer;
Mon, May 22, 8:10 PM
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…
Mon, May 22, 8:10 PM
makarius committed rISABELLEbf4d535bbfcc: clarified build options: reduce heap size by approx. 3%;.
clarified build options: reduce heap size by approx. 3%;
Mon, May 22, 8:10 PM
makarius committed rISABELLE6c6eae08ff87: tuned;.
tuned;
Mon, May 22, 8:10 PM
makarius committed rISABELLEfc5761f07da5: tuned;.
tuned;
Mon, May 22, 8:10 PM
makarius committed rISABELLE1828b174768e: proper Thm.trim_context / Thm.transfer;.
proper Thm.trim_context / Thm.transfer;
Mon, May 22, 8:10 PM
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;
Mon, May 22, 8:10 PM
makarius committed rISABELLE6200555461c6: proper Thm.trim_context / Thm.transfer;.
proper Thm.trim_context / Thm.transfer;
Mon, May 22, 8:10 PM

Fri, May 12

makarius committed rISABELLE2594319ad9ee: proper Thm.trim_context / Thm.transfer;.
proper Thm.trim_context / Thm.transfer;
Fri, May 12, 11:19 PM
makarius committed rISABELLEbd5f6cee8001: proper position for ML-like commands;.
proper position for ML-like commands;
Fri, May 12, 11:19 PM
makarius committed rAFPd640dcca7ba6: adapted to Isabelle/f78cdc6fe971;.
adapted to Isabelle/f78cdc6fe971;
Fri, May 12, 11:17 PM
makarius committed rAFP1fa40be88c80: adapted to Isabelle/f78cdc6fe971;.
adapted to Isabelle/f78cdc6fe971;
Fri, May 12, 11:17 PM

Thu, May 11

makarius committed rISABELLE37085099e415: more robust: after shutdown;.
more robust: after shutdown;
Thu, May 11, 3:17 PM
makarius committed rISABELLE9c18535a9fcd: proper exception CONTEXT for Context.certificate_theory;.
proper exception CONTEXT for Context.certificate_theory;
Thu, May 11, 3:17 PM
makarius committed rISABELLE73c77db63594: more diagnostic operations;.
more diagnostic operations;
Thu, May 11, 3:17 PM
makarius committed rISABELLEec9840c673c3: more standard treatment of data and context;.
more standard treatment of data and context;
Thu, May 11, 3:17 PM
makarius committed rISABELLEa526f69145ec: tuned spelling;.
tuned spelling;
Thu, May 11, 3:17 PM
makarius committed rISABELLE0ee49c509fea: tuned;.
tuned;
Thu, May 11, 3:17 PM
makarius committed rISABELLEf78cdc6fe971: more standard val silent = Attrib.setup_config_bool;.
more standard val silent = Attrib.setup_config_bool;
Thu, May 11, 3:17 PM
makarius committed rAFPad29f283d9c5: adapted to 3f354d5bbf98;.
adapted to 3f354d5bbf98;
Thu, May 11, 11:28 AM

Wed, May 10

makarius committed rISABELLE51d135645d70: tuned;.
tuned;
Wed, May 10, 11:44 PM
makarius committed rISABELLEaf3f1a4ba6e4: proper Thm.trim_context / Thm.transfer;.
proper Thm.trim_context / Thm.transfer;
Wed, May 10, 11:44 PM