isabelle: Graph

reuse SSH.Server connection database server;
18 months ago, by wenzelm
tuned output;
18 months ago, by wenzelm
make double-sure that this is a transaction context, notably for LOCK TABLE;
18 months ago, by wenzelm
more robust Java/Scala multithreading: transaction is always connection.synchronized;
18 months ago, by wenzelm
clarified signature: proper Scala function for command-line tool;
18 months ago, by wenzelm
tuned signature;
18 months ago, by wenzelm
clarified signature: more operations;
18 months ago, by wenzelm
more standard time unit;
18 months ago, by wenzelm
clarified options;
18 months ago, by wenzelm
tuned output;
18 months ago, by wenzelm
global transaction_count;
18 months ago, by wenzelm
tuned output;
18 months ago, by wenzelm
tuned output;
18 months ago, by wenzelm
prefer asynchronous operations: reduce time spent within synchronized_database("Build_Process.start_job");
18 months ago, by wenzelm
clarified isabelle.transaction_log: support time_min (in ms);
18 months ago, by wenzelm
more operations;
18 months ago, by wenzelm
more informative trace;
18 months ago, by wenzelm
support trace of transaction_lock via property "isabelle.transaction_log";
18 months ago, by wenzelm
proper db.transaction_lock instead of adhoc clone (amending 2df0f3604a67);
18 months ago, by wenzelm
tuned;
18 months ago, by wenzelm
proper close() operation;
18 months ago, by wenzelm
tuned comments;
18 months ago, by wenzelm
more robust: avoid nested transactions (on disjoint tables);
18 months ago, by wenzelm
potentially more robust: long-running operation only for build master, not workers;
18 months ago, by wenzelm
less ambitions transactions (amending 3f3dcf9f53f1): TRANSACTION_SERIALIZABLE may lead to spurious rollback exceptions;
18 months ago, by wenzelm
clarified signature: more operations;
18 months ago, by wenzelm
clarified signature: more operations;
18 months ago, by wenzelm
clarified signature;
18 months ago, by wenzelm
clarified signature;
18 months ago, by wenzelm
clarified signature: follow Store.open_database;
18 months ago, by wenzelm
tuned;
18 months ago, by wenzelm
clarified signature;
18 months ago, by wenzelm
clarified signature: more uniform SSH.Port_Forwarding;
18 months ago, by wenzelm
tuned signature;
18 months ago, by wenzelm
X = trivial_topology rather than topspace X = {}
18 months ago, by paulson
merged
18 months ago, by paulson
trivial_topology
18 months ago, by paulson
merged;
18 months ago, by Lukas Stevens
added docs for order method in Orderings;
18 months ago, by Lukas Stevens
News update referring to Analysis
18 months ago, by paulson
tuned error message;
18 months ago, by Fabian Huch
more NEWS;
18 months ago, by wenzelm
tuned output;
18 months ago, by wenzelm
tuned output;
18 months ago, by wenzelm
clarified session_statistics: removed somewhat pointless per-theory statistics;
18 months ago, by wenzelm
tuned error messages;
18 months ago, by Fabian Huch
more TOML formatting functions;
18 months ago, by Fabian Huch
merged
18 months ago, by paulson
Doubled the time limit for HOL-Probability
18 months ago, by paulson
merged
18 months ago, by paulson
Some fixes, and SOME TIME LIMITS
18 months ago, by paulson
merged
18 months ago, by paulson
cosmetic improvements, new lemmas, especially more uses of function space
18 months ago, by paulson
more NEWS;
18 months ago, by wenzelm
NEWS;
18 months ago, by wenzelm
tuned whitespace;
18 months ago, by wenzelm
added TOML module from afp;
18 months ago, by Fabian Huch
proper system integration and renaming;
18 months ago, by wenzelm
copy/rename files from private autocorres version e45b9b680d3e;
18 months ago, by wenzelm
Added tag Isabelle2023-RC1 for changeset 006dbc9c2de1
18 months ago, by wenzelm
update cygwin component;
18 months ago, by wenzelm
avoid bloat of approx. 300MB due to implicit dependency on python;
18 months ago, by wenzelm
suppress bad file, which does not work on regular Windows;
18 months ago, by wenzelm
revert ineffective b04ac8a017b2: etc/settings of polyml components needs to be changed as well;
18 months ago, by wenzelm
updated naproche-20230711 component for release;
18 months ago, by wenzelm
clarified signature;
18 months ago, by wenzelm
ML_system_apple=false for more stability;
18 months ago, by wenzelm
activate cygwin-20230711;
18 months ago, by wenzelm
update cygwin for Isabelle2023 -- somewhere after cygwin 3.4.0-1 (see https://cygwin.com/pipermail/cygwin-announce/2022-December/010821.html);
18 months ago, by wenzelm
proper set_executable for sqlitejdbc.dll (see also 3b0f8f1010f2);
18 months ago, by wenzelm
update to stack-2.9.3 with support for arm64-linux;
18 months ago, by wenzelm
provide tool for GHC stack component;
18 months ago, by wenzelm
tuned signature;
18 months ago, by wenzelm
"rlwrap" is back together with "perl", which is actually required for bib2xhtml;
18 months ago, by wenzelm
clarified signature, with subtle change of semantics (amending 8b5a2e4b16d4);
18 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
merged
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
update for release;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
update for release;
19 months ago, by wenzelm
merged;
19 months ago, by wenzelm
publish component;
19 months ago, by wenzelm
latest version;
19 months ago, by wenzelm
update to current sqlite-jdbc-3.42.0.0;
19 months ago, by wenzelm
update to current lipics-3.1.3;
19 months ago, by wenzelm
update to flatlaf-2.6, which is the last release before recent moves towards 3.0 / 3.1 / 3.1.1;
19 months ago, by wenzelm
merged
19 months ago, by paulson
more small simplifications
19 months ago, by paulson
merged
19 months ago, by wenzelm
merged
19 months ago, by wenzelm
clarified modules (amending 570f65953173);
19 months ago, by wenzelm
more markup for command_span: this allows to reconstruct Thy_Element structure without knowing the outer syntax;
19 months ago, by wenzelm
create database view for diagnostic purposes;
19 months ago, by wenzelm
A bit of prerelease tidying
19 months ago, by paulson
NEWS tweak
19 months ago, by paulson
merged
19 months ago, by paulson
Last of the HOL Light metric space imports, and some supporting lemmas
19 months ago, by paulson
clarified "vacuum" operation for various database versions (PostgreSQL <= 10 is strictly speaking obsolete, but still used on some test machines);
19 months ago, by wenzelm
eliminate somewhat obsolete augment_tables (see ff164add75cd), to support obsolete versions 10 and 9.x;
19 months ago, by wenzelm
clarified operation: sequential vacuum to support obsolete versions 10 and 9.x;
19 months ago, by wenzelm
clarified operation: empty means "empty" instead of "full";
19 months ago, by wenzelm
merged
19 months ago, by wenzelm
proper data_domain for symmetric difference;
19 months ago, by wenzelm
tuned: avoid redundant db access;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
proper transaction_lock;
19 months ago, by wenzelm
clarified signature: ensure disjoint data spaces;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
unused (see also ea35afdb1366);
19 months ago, by wenzelm
more robust transaction_lock: avoid overlapping data spaces;
19 months ago, by wenzelm
merged
19 months ago, by paulson
The sym_diff operator (symmetric difference)
19 months ago, by paulson
disable lxbroy10 for now: technical problems with cooling;
19 months ago, by wenzelm
A couple of new lemmas involving cardinality
19 months ago, by paulson
merged
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
more robust;
19 months ago, by wenzelm
proper build_progress for local messages;
19 months ago, by wenzelm
proper SQL query;
19 months ago, by wenzelm
Another tranche of HOL Light material on metric and topological spaces
19 months ago, by paulson
merged
19 months ago, by paulson
EXPERIMENTAL replacement of f ` A <= B by f : A -> B in Analysis
19 months ago, by paulson
merged
19 months ago, by wenzelm
more robust "stop": further "stamp" ticks may happen afterwards;
19 months ago, by wenzelm
removed junk;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
tuned: prefer Scala over Java;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
more SQL data;
19 months ago, by wenzelm
add proof method "order" to command "try0"
19 months ago, by desharna
tuned signature;
19 months ago, by wenzelm
clarified static Build_Process.Context vs. dynamic Build_Process.State;
19 months ago, by wenzelm
tuned signature: more operations;
19 months ago, by wenzelm
clarified signature: proper equals/hashCode;
19 months ago, by wenzelm
more robust database setup;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
New theory Leftist_Heap_List
19 months ago, by nipkow
added [simp]
19 months ago, by nipkow
merged
19 months ago, by wenzelm
proper build_master.build_uuid;
19 months ago, by wenzelm
proper session_init *after* deleting db files (amending af6c493b0441);
19 months ago, by wenzelm
clarified signature: more concise data;
19 months ago, by wenzelm
tuned output;
19 months ago, by wenzelm
more robust;
19 months ago, by wenzelm
clarified signature: better default;
19 months ago, by wenzelm
show only active builds;
19 months ago, by wenzelm
clarified output;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
support for identified builds;
19 months ago, by wenzelm
clarified signature: more operations and options;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
more robust close() after failed initialization;
19 months ago, by wenzelm
avoid repeated open_database_server: synchronized transaction_lock;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
more robust: proper transaction_lock;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
clarified signature: more options;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
clarified database for heaps: do not depend on build_database_test;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
More metric space material
19 months ago, by paulson
merged
19 months ago, by paulson
New and generalised analysis lemmas
19 months ago, by paulson
tuned names
19 months ago, by nipkow
clarified signature: prefer explicit combinator;
19 months ago, by wenzelm
unused;
19 months ago, by wenzelm
restore heaps from database, which takes precedence over file-system;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
more operations;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
more robust try-finally;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
proper clean_entry;
19 months ago, by wenzelm
afford larger build_database_slice for better compression (HOL: 1 slice, HOL-Proofs: multiple slices for testing);
19 months ago, by wenzelm
prefer system option;
19 months ago, by wenzelm
clarified signature: more explicit class SQL.Data;
19 months ago, by wenzelm
proper ML_Heap.clean_entry;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
store heaps within database server;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
clarified modules;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
clarified modules;
19 months ago, by wenzelm
clarified modules;
19 months ago, by wenzelm
early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals;
19 months ago, by Mathias Fleury
merged
19 months ago, by wenzelm
proper close;
19 months ago, by wenzelm
separate host.db for independent db.transaction_lock;
19 months ago, by wenzelm
tuned comments;
19 months ago, by wenzelm
omit redundant data: already stored in progress database;
19 months ago, by wenzelm
tuned signature: more operations;
19 months ago, by wenzelm
proper support for SQLite: avoid conflicts on transaction_lock;
19 months ago, by wenzelm
minor performance tuning: avoid external process;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
obsolete;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
proper pattern (amending da5cc332ded3);
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
proper hostname from build_context;
19 months ago, by wenzelm
prefer Database_Progress, which is more robust (amending afb1a19307c4);
19 months ago, by wenzelm
support for Database_Progress;
19 months ago, by wenzelm
tuned signature: more operations;
19 months ago, by wenzelm
tuned signature: more operations;
19 months ago, by wenzelm
tuned signature: more operations;
19 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
optional description in Eisbach "method" command;
19 months ago, by kleing
disable 'falsify' and 'abduce' in Sledgehammer by default, since they don't seem to be very useful in practice
19 months ago, by blanchet
Added tag Isabelle2023-RC0 for changeset f4221ae7544c
20 months ago, by wenzelm
updated to zstd-jni-1.5.5-4;
20 months ago, by wenzelm
updated to postgresql-42.6.0;
20 months ago, by wenzelm
back to more concise build_release, thanks to build_host_macos = "mini3";
20 months ago, by wenzelm
more PLATFORMS;
20 months ago, by wenzelm
updated for release;
20 months ago, by wenzelm
tuned NEWS;
20 months ago, by wenzelm
more realistic factor;
20 months ago, by wenzelm
proper trim_context;
20 months ago, by wenzelm
proper exception positions;
20 months ago, by wenzelm
proper trim_context / transfer, e.g. for Specification.definition;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned signature: more operations;
20 months ago, by wenzelm
minor performance tuning: avoid append to end-of-list;
20 months ago, by wenzelm
TN has enough examples of the bug.
20 months ago, by nipkow
added lemma ffUnion_fsubset_iff
20 months ago, by desharna
Even more material from the HOL Light metric space library
20 months ago, by paulson
NEWS: Announcing the metric space material
20 months ago, by paulson
merged
20 months ago, by paulson
Hiding the constructor names, particularly to avoid conflicts involving "ext"
20 months ago, by paulson
New HOL Light material on metric spaces and topological spaces
20 months ago, by paulson
enable scala-3.3.0, with forced rebuild of Isabelle/Scala and Isabelle/ML;
20 months ago, by wenzelm
provide scala-3.3.0;
20 months ago, by wenzelm
more NEWS;
20 months ago, by wenzelm
tuned NEWS;
20 months ago, by wenzelm
NEWS;
20 months ago, by wenzelm
removed intro, desc, elim, and simp annotations from FSet lemmas that are instances of lemmas in Set
20 months ago, by desharna
merged
20 months ago, by desharna
NEWS
20 months ago, by desharna
set up code generation for fset
20 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
20 months ago, by wenzelm
tuned signature;
20 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;
21 months ago, by wenzelm
proper position for ML-like commands;
21 months ago, by wenzelm
more robust: after shutdown;
21 months ago, by wenzelm
proper exception CONTEXT for Context.certificate_theory;
21 months ago, by wenzelm
more diagnostic operations;
21 months ago, by wenzelm
tuned spelling;
21 months ago, by wenzelm
more standard treatment of data and context;
21 months ago, by wenzelm
more standard val silent = Attrib.setup_config_bool;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
proper Thm.trim_context / Thm.transfer;
21 months ago, by wenzelm
proper Thm.trim_context / Thm.transfer;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
tuned Isabelle/ML;
21 months ago, by wenzelm
more informative position information;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
more informative position information;
21 months ago, by wenzelm
clarified context tracing;
21 months ago, by wenzelm
more operations;
21 months ago, by wenzelm
proper system options to control context tracing/timing;
21 months ago, by wenzelm
added lemmas transp_on_multpHO and transp_multpHO
21 months ago, by desharna
tuned theory structure
21 months ago, by desharna
merged
21 months ago, by desharna
added lemmas Finite_Set.bex_(min|max)_element_with_property and reordered assumptions of Finite_Set.bex_(min|max)_element
21 months ago, by desharna
backed out changeset 6c2494750a4e: it hardly makes a difference for heap size, but crashes arm64_32-darwin for unknown reasons;
21 months ago, by wenzelm
enforce rebuild of Isabelle/ML + Isabelle/Scala;
21 months ago, by wenzelm
updated to jdk-17.0.7;
21 months ago, by wenzelm
minor performance tuning (see also f906f7f83dae and b23c42b9f78a);
21 months ago, by wenzelm
performance tuning: cached non-persistent Parser.gram reduces heap size by approx. 1-4%;
21 months ago, by wenzelm
more operations;
21 months ago, by wenzelm
tuned: more readable ML;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
backed out changeset 4660181c83c9: remove rather pointless timing (1..50ms);
21 months ago, by wenzelm
maintain dynamic position where values are created (again, amending afa6117bace4);
21 months ago, by wenzelm
more robust: publish token only after assignment of result;
21 months ago, by wenzelm
tuned comments;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
merged
21 months ago, by wenzelm
tuned signature;
21 months ago, by wenzelm
support for cached evaluation via weak_ref;
21 months ago, by wenzelm
optional timing;
21 months ago, by wenzelm
more informative trace of context allocations;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
tuned internal structure;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
tuned whitespace;
21 months ago, by wenzelm
merged
21 months ago, by desharna
added author
21 months ago, by desharna
added lemma asymp_on_multpHO
21 months ago, by desharna
added lemmas multpHO_iff_set_mset_lessHO_set_mset and multpHO_minus_inter_minus_inter_iff
21 months ago, by desharna
added lemmas count_minus_inter_lt_count_minus_inter_iff and minus_inter_eq_minus_inter_iff
21 months ago, by desharna
added lemma multpHO_implies_one_step_strong
21 months ago, by desharna
merged
21 months ago, by wenzelm
tuned comments;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
hide names more thorougly, in contrast to 1d82061fbb12 and 00e9ca1e7261: e.g. relevant for overlapping accesses seen in 'inductive_set';
21 months ago, by wenzelm
minor performance tuning;
21 months ago, by wenzelm
minor performance tuning;
21 months ago, by wenzelm
back to more elementary concept of aliases as adhoc change of accesses, but now with "suppress" information (see also 31ea5c1f874d);
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
clarified data representation: slightly more compact, since internals_hidden is sparesely populated and rarely changes;
21 months ago, by wenzelm
more operations;
21 months ago, by wenzelm
more operations;
21 months ago, by wenzelm
more operations;
21 months ago, by wenzelm
minor performance tuning;
21 months ago, by wenzelm
unused;
21 months ago, by wenzelm
more complete accesses for "extern" operation, notably for aliases;
21 months ago, by wenzelm
more explicit entries for aliases, with proper checks in "strict" mode (e.g. for logical entities);
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
unused;
21 months ago, by wenzelm
minor performance tuning;
21 months ago, by wenzelm
tuned signature;
21 months ago, by wenzelm
minor performance tuning;
21 months ago, by wenzelm
revert pointless performance tuning fd5f4455e033: no measurable difference in HOL, HOL-Library, HOL-Analysis;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
more accurate treatment of traditional name space accesses (refining 948f5dc4d694, fcd85e04a948, 238307775d52);
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
proper treatment of restriction (for 'qualified');
21 months ago, by wenzelm
misc tuning;
21 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;
21 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;
21 months ago, by wenzelm
minor performance tuning: more compact representation of only sparsely table;
21 months ago, by wenzelm
minor performance tuning: no storage of accesses, produce Binding.full_name_spec on the spot;
21 months ago, by wenzelm
proper checks;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
tuned structure;
21 months ago, by wenzelm
tuned signature;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
clarified extern vs. alias/hide: output alternative names, if possible;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
minor performance tuning: more compact, more sharing;
21 months ago, by wenzelm
potential performance tuning: more compact data structure, but less sharing;
21 months ago, by wenzelm
Importation of additional lemmas from metric.ml
21 months ago, by paulson
fixes esp to theory presentation
21 months ago, by paulson
new material ported from HOL Light's metric.ml
21 months ago, by paulson
merged
21 months ago, by paulson
Two new theories containing material ported from HOL Light about abstract topology
21 months ago, by paulson
merged
21 months ago, by nipkow
streamlined
21 months ago, by nipkow
merged
21 months ago, by paulson
More new theorems, and a necessary correction
21 months ago, by paulson
A few new theorems
21 months ago, by paulson
merged
21 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
21 months ago, by haftmann
tuned
21 months ago, by haftmann
case translation in intermediate language eliminates semantic clone
21 months ago, by haftmann
minor performance tuning;
21 months ago, by wenzelm
more correct type calculation
21 months ago, by haftmann
Backed out changeset 5016262a2384
21 months ago, by haftmann
added lemma
21 months ago, by nipkow
thingol: fix abstraction return types in case
21 months ago, by stuebinm
merged
21 months ago, by desharna
tuned; avoided intermediate lists
21 months ago, by desharna
tuned; avoided intermediate list and list traversal
21 months ago, by desharna
tuned; avoided intermediate lists
21 months ago, by desharna
tuned; avoided intermediate list
21 months ago, by desharna
made 'primcorec' more robust
21 months ago, by blanchet
performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
21 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
proper Thm.trim_context / Thm.transfer for context data;
21 months ago, by wenzelm
tuned: more concise data record;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
clarified counters and types;
21 months ago, by wenzelm
tuned signature;
21 months ago, by wenzelm
support n-ary merge theory data;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm