Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
proper trim_context;
19 months ago, by wenzelm
proper exception positions;
19 months ago, by wenzelm
proper trim_context / transfer, e.g. for Specification.definition;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
tuned signature: more operations;
19 months ago, by wenzelm
minor performance tuning: avoid append to end-of-list;
19 months ago, by wenzelm
TN has enough examples of the bug.
19 months ago, by nipkow
added lemma ffUnion_fsubset_iff
19 months ago, by desharna
Even more material from the HOL Light metric space library
19 months ago, by paulson
NEWS: Announcing the metric space material
19 months ago, by paulson
merged
19 months ago, by paulson
Hiding the constructor names, particularly to avoid conflicts involving "ext"
19 months ago, by paulson
New HOL Light material on metric spaces and topological spaces
19 months ago, by paulson
enable scala-3.3.0, with forced rebuild of Isabelle/Scala and Isabelle/ML;
19 months ago, by wenzelm
provide scala-3.3.0;
19 months ago, by wenzelm
more NEWS;
19 months ago, by wenzelm
tuned NEWS;
19 months ago, by wenzelm
NEWS;
19 months ago, by wenzelm
removed intro, desc, elim, and simp annotations from FSet lemmas that are instances of lemmas in Set
19 months ago, by desharna
merged
19 months ago, by desharna
NEWS
19 months ago, by desharna
set up code generation for fset
19 months ago, by desharna
redefined FSet.fBall and FSet.fBex as abbreviations based on Set.Ball and Set.Bex
20 months ago, by desharna
merged
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
clarified treatment of context;
20 months ago, by wenzelm
clarified treatment of context;
20 months ago, by wenzelm
more operations;
20 months ago, by wenzelm
NEWS
20 months ago, by desharna
renamed notin_fset to not_fmember
20 months ago, by desharna
added author
20 months ago, by desharna
merged
20 months ago, by desharna
adapted Transfer_Debug from fmember to fempty
20 months ago, by desharna
renamed variables
20 months ago, by desharna
merged
20 months ago, by desharna
fixed lemma name
20 months ago, by desharna
redefined FSet.fmember as an abbreviation based on Set.member
20 months ago, by desharna
replaced some lemmas' implicit formulas by explicit ones to avoid silent changes
20 months ago, by desharna
merged
20 months ago, by wenzelm
proper setup for rule attribute;
20 months ago, by wenzelm
more uniform simproc_setup: avoid vacuous abstraction over morphism, which sometimes captures context values in its functional closure;
20 months ago, by wenzelm
clarified output of embedded values, e.g. for 'print_locale';
20 months ago, by wenzelm
tuned: more antiquotations;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned signature: more position information;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
Finally, the abstract metric space development
20 months ago, by paulson
merged
20 months ago, by wenzelm
misc tuning and clarification;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned --- Token.make_string / Token.assign are value-oriented;
20 months ago, by wenzelm
more documentation;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
more robust context: fail immediately via Morphism.the_theory, instead of rarely via Thm.theory_of_thm (for non-normal thm);
20 months ago, by wenzelm
prefer static simpset;
20 months ago, by wenzelm
omit pointless morphism in global theory;
20 months ago, by wenzelm
more operations;
20 months ago, by wenzelm
more careful treatment of context for method source;
20 months ago, by wenzelm
clarified context;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
remove pointless context setup (see also b2e449c155a4);
20 months ago, by wenzelm
more careful reset_context for stored entity;
20 months ago, by wenzelm
more careful reset/set_context for stored declarations;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
clarified signature: more explicit types;
20 months ago, by wenzelm
clarified data: avoid pointless Morphism.transform;
20 months ago, by wenzelm
proper Token.Declaration for internal_declaration;
20 months ago, by wenzelm
more standard treatment of morphism context;
20 months ago, by wenzelm
tuned: avoid duplication;
20 months ago, by wenzelm
more standard treatment of morphism context, but hardly relevant here;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
more careful treatment of set_context / reset_context for persistent morphisms;
20 months ago, by wenzelm
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
support for context within morphism (for background theory);
20 months ago, by wenzelm
proper transfer to supported "bundle ... begin unbundle ... end", e.g. see theory "AFP/Probabilistic_Timed_Automata.Graphs";
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
more accurate Thm.trim_context / Thm.transfer;
20 months ago, by wenzelm
clarified stored thm: result from notes;
20 months ago, by wenzelm
tuned whitespace;
20 months ago, by wenzelm
clarified signature: avoid convoluted operations;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
update to polyml-a5d5fba90286, with more robust ML_Heap.sizeof;
20 months ago, by wenzelm
avoid capture of inner/outer context and thus reduce heaps sizes by 20..40% (see also dd04a8b654fc, e49bf4ebf330, 9c19e15c8548, 71467e35fc3c);
20 months ago, by wenzelm
proper transfer / trim_context;
20 months ago, by wenzelm
more operations "without_context", assuming that the thm has been properly transferred already;
20 months ago, by wenzelm
proper trim_context / transfer;
20 months ago, by wenzelm
tuned: more accurate check (is_norm_hhf protect);
20 months ago, by wenzelm
clarified build options: reduce heap size by approx. 3%;
20 months ago, by wenzelm
more standard merge order, following logical structure of imports rather than physical serials;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
proper Thm.trim_context / Thm.transfer;
20 months ago, by wenzelm
proper Thm.trim_context / Thm.transfer;
20 months ago, by wenzelm
tuned: avoid pointless Proof_Context.init_global of Context.proof_of;
20 months ago, by wenzelm
New material from the HOL Light metric space library, mostly about quasi components
20 months ago, by paulson
More material from the HOL Light metric space library
20 months ago, by paulson
proper Thm.trim_context / Thm.transfer;
20 months ago, by wenzelm
proper position for ML-like commands;
20 months ago, by wenzelm
more robust: after shutdown;
20 months ago, by wenzelm
proper exception CONTEXT for Context.certificate_theory;
20 months ago, by wenzelm
more diagnostic operations;
20 months ago, by wenzelm
tuned spelling;
20 months ago, by wenzelm
more standard treatment of data and context;
20 months ago, by wenzelm
more standard val silent = Attrib.setup_config_bool;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
proper Thm.trim_context / Thm.transfer;
20 months ago, by wenzelm
proper Thm.trim_context / Thm.transfer;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned Isabelle/ML;
20 months ago, by wenzelm
more informative position information;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
more informative position information;
20 months ago, by wenzelm
clarified context tracing;
20 months ago, by wenzelm
more operations;
20 months ago, by wenzelm
proper system options to control context tracing/timing;
20 months ago, by wenzelm
added lemmas transp_on_multpHO and transp_multpHO
20 months ago, by desharna
tuned theory structure
20 months ago, by desharna
merged
20 months ago, by desharna
added lemmas Finite_Set.bex_(min|max)_element_with_property and reordered assumptions of Finite_Set.bex_(min|max)_element
20 months ago, by desharna
backed out changeset 6c2494750a4e: it hardly makes a difference for heap size, but crashes arm64_32-darwin for unknown reasons;
20 months ago, by wenzelm
enforce rebuild of Isabelle/ML + Isabelle/Scala;
20 months ago, by wenzelm
updated to jdk-17.0.7;
20 months ago, by wenzelm
minor performance tuning (see also f906f7f83dae and b23c42b9f78a);
20 months ago, by wenzelm
performance tuning: cached non-persistent Parser.gram reduces heap size by approx. 1-4%;
20 months ago, by wenzelm
more operations;
20 months ago, by wenzelm
tuned: more readable ML;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
backed out changeset 4660181c83c9: remove rather pointless timing (1..50ms);
20 months ago, by wenzelm
maintain dynamic position where values are created (again, amending afa6117bace4);
20 months ago, by wenzelm
more robust: publish token only after assignment of result;
20 months ago, by wenzelm
tuned comments;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
merged
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
support for cached evaluation via weak_ref;
20 months ago, by wenzelm
optional timing;
20 months ago, by wenzelm
more informative trace of context allocations;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned internal structure;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned whitespace;
20 months ago, by wenzelm
merged
20 months ago, by desharna
added author
20 months ago, by desharna
added lemma asymp_on_multpHO
20 months ago, by desharna
added lemmas multpHO_iff_set_mset_lessHO_set_mset and multpHO_minus_inter_minus_inter_iff
20 months ago, by desharna
added lemmas count_minus_inter_lt_count_minus_inter_iff and minus_inter_eq_minus_inter_iff
20 months ago, by desharna
added lemma multpHO_implies_one_step_strong
20 months ago, by desharna
merged
20 months ago, by wenzelm
tuned comments;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
hide names more thorougly, in contrast to 1d82061fbb12 and 00e9ca1e7261: e.g. relevant for overlapping accesses seen in 'inductive_set';
20 months ago, by wenzelm
minor performance tuning;
20 months ago, by wenzelm
minor performance tuning;
20 months ago, by wenzelm
back to more elementary concept of aliases as adhoc change of accesses, but now with "suppress" information (see also 31ea5c1f874d);
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
clarified data representation: slightly more compact, since internals_hidden is sparesely populated and rarely changes;
20 months ago, by wenzelm
more operations;
20 months ago, by wenzelm
more operations;
20 months ago, by wenzelm
more operations;
20 months ago, by wenzelm
minor performance tuning;
20 months ago, by wenzelm
unused;
20 months ago, by wenzelm
more complete accesses for "extern" operation, notably for aliases;
20 months ago, by wenzelm
more explicit entries for aliases, with proper checks in "strict" mode (e.g. for logical entities);
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
unused;
20 months ago, by wenzelm
minor performance tuning;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
minor performance tuning;
20 months ago, by wenzelm
revert pointless performance tuning fd5f4455e033: no measurable difference in HOL, HOL-Library, HOL-Analysis;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
more accurate treatment of traditional name space accesses (refining 948f5dc4d694, fcd85e04a948, 238307775d52);
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
proper treatment of restriction (for 'qualified');
20 months ago, by wenzelm
misc tuning;
20 months ago, by wenzelm
more complete accesses for hide operation (amending fcd85e04a948), e.g. relevant for AFP/thys/Jordan_Normal_Form/Matrix_Kernel.thy in AFP/4d8afd37b465;
20 months ago, by wenzelm
more standard name bindings (amending 5bf71b4da706): avoid odd full_name like "Orderings.class.Orderings.preorder.of_class.intro" with many redundant name space accesses;
20 months ago, by wenzelm
minor performance tuning: more compact representation of only sparsely table;
20 months ago, by wenzelm
minor performance tuning: no storage of accesses, produce Binding.full_name_spec on the spot;
20 months ago, by wenzelm
proper checks;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned structure;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
clarified extern vs. alias/hide: output alternative names, if possible;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
minor performance tuning: more compact, more sharing;
20 months ago, by wenzelm
potential performance tuning: more compact data structure, but less sharing;
20 months ago, by wenzelm
Importation of additional lemmas from metric.ml
20 months ago, by paulson
fixes esp to theory presentation
20 months ago, by paulson
new material ported from HOL Light's metric.ml
20 months ago, by paulson
merged
20 months ago, by paulson
Two new theories containing material ported from HOL Light about abstract topology
20 months ago, by paulson
merged
20 months ago, by nipkow
streamlined
20 months ago, by nipkow
merged
20 months ago, by paulson
More new theorems, and a necessary correction
20 months ago, by paulson
A few new theorems
20 months ago, by paulson
merged
20 months ago, by paulson
merged
21 months ago, by paulson
merged
21 months ago, by paulson
merged
22 months ago, by paulson
Numerous significant simplifications
22 months ago, by paulson
stripped unused functionality
20 months ago, by haftmann
tuned
20 months ago, by haftmann
case translation in intermediate language eliminates semantic clone
20 months ago, by haftmann
minor performance tuning;
20 months ago, by wenzelm
more correct type calculation
20 months ago, by haftmann
Backed out changeset 5016262a2384
20 months ago, by haftmann
added lemma
20 months ago, by nipkow
thingol: fix abstraction return types in case
20 months ago, by stuebinm
merged
20 months ago, by desharna
tuned; avoided intermediate lists
20 months ago, by desharna
tuned; avoided intermediate list and list traversal
20 months ago, by desharna
tuned; avoided intermediate lists
20 months ago, by desharna
tuned; avoided intermediate list
20 months ago, by desharna
made 'primcorec' more robust
20 months ago, by blanchet
performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
20 months ago, by wenzelm
tuned signature;
21 months ago, by wenzelm
more operations for lexicographic ordering;
21 months ago, by wenzelm
more operations: following Library list operations and Ord_List.T operations;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
tuned: concise combinators instead of bulky case-expressions;
21 months ago, by wenzelm
provide ML antiquotation "if_none": non-strict version of "the_default";
21 months ago, by wenzelm
merged
21 months ago, by wenzelm
proper Thm.trim_context / Thm.transfer (see also 0d401f874942);
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
more operations;
21 months ago, by wenzelm
more operations;
21 months ago, by wenzelm
more uniform operations wrt. Thm.full_prop_of;
21 months ago, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
tip