isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 tip

merged
2023-05-25, by wenzelm
proper setup for rule attribute;
2023-05-23, by wenzelm
more uniform simproc_setup: avoid vacuous abstraction over morphism, which sometimes captures context values in its functional closure;
2023-05-23, by wenzelm
clarified output of embedded values, e.g. for 'print_locale';
2023-05-23, by wenzelm
tuned: more antiquotations;
2023-05-23, by wenzelm
tuned;
2023-05-23, by wenzelm
tuned signature: more position information;
2023-05-23, by wenzelm
tuned;
2023-05-23, by wenzelm
Finally, the abstract metric space development
2023-05-23, by paulson
merged
2023-05-22, by wenzelm
misc tuning and clarification;
2023-05-20, by wenzelm
tuned signature;
2023-05-20, by wenzelm
tuned;
2023-05-20, by wenzelm
tuned --- Token.make_string / Token.assign are value-oriented;
2023-05-20, by wenzelm
more documentation;
2023-05-20, by wenzelm
tuned signature;
2023-05-20, by wenzelm
tuned signature;
2023-05-20, by wenzelm
more robust context: fail immediately via Morphism.the_theory, instead of rarely via Thm.theory_of_thm (for non-normal thm);
2023-05-20, by wenzelm
prefer static simpset;
2023-05-20, by wenzelm
omit pointless morphism in global theory;
2023-05-20, by wenzelm
more operations;
2023-05-20, by wenzelm
more careful treatment of context for method source;
2023-05-19, by wenzelm
clarified context;
2023-05-19, by wenzelm
clarified signature;
2023-05-19, by wenzelm
remove pointless context setup (see also b2e449c155a4);
2023-05-19, by wenzelm
more careful reset_context for stored entity;
2023-05-19, by wenzelm
more careful reset/set_context for stored declarations;
2023-05-18, by wenzelm
tuned;
2023-05-18, by wenzelm
tuned;
2023-05-18, by wenzelm
clarified signature: more explicit types;
2023-05-18, by wenzelm
clarified data: avoid pointless Morphism.transform;
2023-05-18, by wenzelm
proper Token.Declaration for internal_declaration;
2023-05-18, by wenzelm
more standard treatment of morphism context;
2023-05-16, by wenzelm
tuned: avoid duplication;
2023-05-16, by wenzelm
more standard treatment of morphism context, but hardly relevant here;
2023-05-16, by wenzelm
tuned;
2023-05-16, by wenzelm
more careful treatment of set_context / reset_context for persistent morphisms;
2023-05-16, by wenzelm
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
2023-05-16, by wenzelm
tuned signature;
2023-05-16, by wenzelm
support for context within morphism (for background theory);
2023-05-16, by wenzelm
proper transfer to supported "bundle ... begin unbundle ... end", e.g. see theory "AFP/Probabilistic_Timed_Automata.Graphs";
2023-05-15, by wenzelm
clarified signature;
2023-05-15, by wenzelm
tuned;
2023-05-15, by wenzelm
tuned;
2023-05-15, by wenzelm
tuned signature;
2023-05-15, by wenzelm
more accurate Thm.trim_context / Thm.transfer;
2023-05-15, by wenzelm
clarified stored thm: result from notes;
2023-05-15, by wenzelm
tuned whitespace;
2023-05-15, by wenzelm
clarified signature: avoid convoluted operations;
2023-05-15, by wenzelm
tuned signature;
2023-05-15, by wenzelm
update to polyml-a5d5fba90286, with more robust ML_Heap.sizeof;
2023-05-15, by wenzelm
avoid capture of inner/outer context and thus reduce heaps sizes by 20..40% (see also dd04a8b654fc, e49bf4ebf330, 9c19e15c8548, 71467e35fc3c);
2023-05-15, by wenzelm
proper transfer / trim_context;
2023-05-15, by wenzelm
more operations "without_context", assuming that the thm has been properly transferred already;
2023-05-15, by wenzelm
proper trim_context / transfer;
2023-05-15, by wenzelm
tuned: more accurate check (is_norm_hhf protect);
2023-05-15, by wenzelm
clarified build options: reduce heap size by approx. 3%;
2023-05-15, by wenzelm
more standard merge order, following logical structure of imports rather than physical serials;
2023-05-14, by wenzelm
tuned;
2023-05-14, by wenzelm
tuned;
2023-05-14, by wenzelm
proper Thm.trim_context / Thm.transfer;
2023-05-14, by wenzelm
proper Thm.trim_context / Thm.transfer;
2023-05-14, by wenzelm
tuned: avoid pointless Proof_Context.init_global of Context.proof_of;
2023-05-13, by wenzelm
New material from the HOL Light metric space library, mostly about quasi components
2023-05-18, by paulson
More material from the HOL Light metric space library
2023-05-15, by paulson
proper Thm.trim_context / Thm.transfer;
2023-05-11, by wenzelm
proper position for ML-like commands;
2023-05-11, by wenzelm
more robust: after shutdown;
2023-05-11, by wenzelm
proper exception CONTEXT for Context.certificate_theory;
2023-05-11, by wenzelm
more diagnostic operations;
2023-05-11, by wenzelm
tuned spelling;
2023-05-11, by wenzelm
more standard treatment of data and context;
2023-05-10, by wenzelm
more standard val silent = Attrib.setup_config_bool;
2023-05-10, by wenzelm
tuned;
2023-05-10, by wenzelm
proper Thm.trim_context / Thm.transfer;
2023-05-10, by wenzelm
proper Thm.trim_context / Thm.transfer;
2023-05-10, by wenzelm
tuned;
2023-05-10, by wenzelm
tuned Isabelle/ML;
2023-05-10, by wenzelm
more informative position information;
2023-05-10, by wenzelm
tuned;
2023-05-10, by wenzelm
more informative position information;
2023-05-10, by wenzelm
clarified context tracing;
2023-05-10, by wenzelm
more operations;
2023-05-10, by wenzelm
proper system options to control context tracing/timing;
2023-05-10, by wenzelm
added lemmas transp_on_multpHO and transp_multpHO
2023-05-10, by desharna
tuned theory structure
2023-05-10, by desharna
merged
2023-05-10, by desharna
added lemmas Finite_Set.bex_(min|max)_element_with_property and reordered assumptions of Finite_Set.bex_(min|max)_element
2023-05-09, by desharna
backed out changeset 6c2494750a4e: it hardly makes a difference for heap size, but crashes arm64_32-darwin for unknown reasons;
2023-05-09, by wenzelm
enforce rebuild of Isabelle/ML + Isabelle/Scala;
2023-05-09, by wenzelm
updated to jdk-17.0.7;
2023-05-09, by wenzelm
minor performance tuning (see also f906f7f83dae and b23c42b9f78a);
2023-05-09, by wenzelm
performance tuning: cached non-persistent Parser.gram reduces heap size by approx. 1-4%;
2023-05-09, by wenzelm
more operations;
2023-05-09, by wenzelm
tuned: more readable ML;
2023-05-09, by wenzelm
tuned;
2023-05-09, by wenzelm
backed out changeset 4660181c83c9: remove rather pointless timing (1..50ms);
2023-05-09, by wenzelm
maintain dynamic position where values are created (again, amending afa6117bace4);
2023-05-09, by wenzelm
more robust: publish token only after assignment of result;
2023-05-09, by wenzelm
tuned comments;
2023-05-09, by wenzelm
clarified signature;
2023-05-09, by wenzelm
merged
2023-05-09, by wenzelm
tuned signature;
2023-05-09, by wenzelm
support for cached evaluation via weak_ref;
2023-05-08, by wenzelm
optional timing;
2023-05-08, by wenzelm
more informative trace of context allocations;
2023-05-08, by wenzelm
tuned;
2023-05-08, by wenzelm
tuned internal structure;
2023-05-08, by wenzelm
tuned;
2023-05-08, by wenzelm
tuned whitespace;
2023-05-08, by wenzelm
merged
2023-05-08, by desharna
added author
2023-05-08, by desharna
added lemma asymp_on_multpHO
2023-05-08, by desharna
added lemmas multpHO_iff_set_mset_lessHO_set_mset and multpHO_minus_inter_minus_inter_iff
2023-05-08, by desharna
added lemmas count_minus_inter_lt_count_minus_inter_iff and minus_inter_eq_minus_inter_iff
2023-05-08, by desharna
added lemma multpHO_implies_one_step_strong
2023-05-08, by desharna
merged
2023-05-07, by wenzelm
tuned comments;
2023-05-07, by wenzelm
tuned;
2023-05-07, by wenzelm
hide names more thorougly, in contrast to 1d82061fbb12 and 00e9ca1e7261: e.g. relevant for overlapping accesses seen in 'inductive_set';
2023-05-07, by wenzelm