Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-1920
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.
NEWS: Announcing the metric space material
default
tip
28 hours ago, by paulson
merged
29 hours ago, by paulson
Hiding the constructor names, particularly to avoid conflicts involving "ext"
2 days ago, by paulson
New HOL Light material on metric spaces and topological spaces
2 days ago, by paulson
enable scala-3.3.0, with forced rebuild of Isabelle/Scala and Isabelle/ML;
30 hours ago, by wenzelm
provide scala-3.3.0;
30 hours ago, by wenzelm
more NEWS;
30 hours ago, by wenzelm
tuned NEWS;
31 hours ago, by wenzelm
NEWS;
2 days ago, by wenzelm
removed intro, desc, elim, and simp annotations from FSet lemmas that are instances of lemmas in Set
4 days ago, by desharna
merged
4 days ago, by desharna
NEWS
4 days ago, by desharna
set up code generation for fset
4 days ago, by desharna
redefined FSet.fBall and FSet.fBex as abbreviations based on Set.Ball and Set.Bex
6 days ago, by desharna
merged
5 days ago, by wenzelm
tuned signature;
5 days ago, by wenzelm
clarified treatment of context;
6 days ago, by wenzelm
clarified treatment of context;
6 days ago, by wenzelm
more operations;
6 days ago, by wenzelm
NEWS
6 days ago, by desharna
renamed notin_fset to not_fmember
6 days ago, by desharna
added author
6 days ago, by desharna
merged
6 days ago, by desharna
adapted Transfer_Debug from fmember to fempty
6 days ago, by desharna
renamed variables
6 days ago, by desharna
merged
2 weeks ago, by desharna
fixed lemma name
2 weeks ago, by desharna
redefined FSet.fmember as an abbreviation based on Set.member
2 weeks ago, by desharna
replaced some lemmas' implicit formulas by explicit ones to avoid silent changes
2 weeks ago, by desharna
merged
7 days ago, by wenzelm
proper setup for rule attribute;
8 days ago, by wenzelm
more uniform simproc_setup: avoid vacuous abstraction over morphism, which sometimes captures context values in its functional closure;
8 days ago, by wenzelm
clarified output of embedded values, e.g. for 'print_locale';
8 days ago, by wenzelm
tuned: more antiquotations;
8 days ago, by wenzelm
tuned;
8 days ago, by wenzelm
tuned signature: more position information;
8 days ago, by wenzelm
tuned;
9 days ago, by wenzelm
Finally, the abstract metric space development
9 days ago, by paulson
merged
10 days ago, by wenzelm
misc tuning and clarification;
11 days ago, by wenzelm
tuned signature;
11 days ago, by wenzelm
tuned;
11 days ago, by wenzelm
tuned --- Token.make_string / Token.assign are value-oriented;
11 days ago, by wenzelm
more documentation;
11 days ago, by wenzelm
tuned signature;
11 days ago, by wenzelm
tuned signature;
12 days ago, by wenzelm
more robust context: fail immediately via Morphism.the_theory, instead of rarely via Thm.theory_of_thm (for non-normal thm);
12 days ago, by wenzelm
prefer static simpset;
12 days ago, by wenzelm
omit pointless morphism in global theory;
12 days ago, by wenzelm
more operations;
12 days ago, by wenzelm
more careful treatment of context for method source;
12 days ago, by wenzelm
clarified context;
12 days ago, by wenzelm
clarified signature;
12 days ago, by wenzelm
remove pointless context setup (see also b2e449c155a4);
13 days ago, by wenzelm
more careful reset_context for stored entity;
13 days ago, by wenzelm
more careful reset/set_context for stored declarations;
13 days ago, by wenzelm
tuned;
13 days ago, by wenzelm
tuned;
13 days ago, by wenzelm
clarified signature: more explicit types;
2 weeks ago, by wenzelm
clarified data: avoid pointless Morphism.transform;
2 weeks ago, by wenzelm
proper Token.Declaration for internal_declaration;
2 weeks ago, by wenzelm
more standard treatment of morphism context;
2 weeks ago, by wenzelm
tuned: avoid duplication;
2 weeks ago, by wenzelm
more standard treatment of morphism context, but hardly relevant here;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
more careful treatment of set_context / reset_context for persistent morphisms;
2 weeks ago, by wenzelm
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
2 weeks ago, by wenzelm
tuned signature;
2 weeks ago, by wenzelm
support for context within morphism (for background theory);
2 weeks ago, by wenzelm
proper transfer to supported "bundle ... begin unbundle ... end", e.g. see theory "AFP/Probabilistic_Timed_Automata.Graphs";
2 weeks ago, by wenzelm
clarified signature;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
tuned signature;
2 weeks ago, by wenzelm
more accurate Thm.trim_context / Thm.transfer;
2 weeks ago, by wenzelm
clarified stored thm: result from notes;
2 weeks ago, by wenzelm
tuned whitespace;
2 weeks ago, by wenzelm
clarified signature: avoid convoluted operations;
2 weeks ago, by wenzelm
tuned signature;
2 weeks ago, by wenzelm
update to polyml-a5d5fba90286, with more robust ML_Heap.sizeof;
2 weeks ago, by wenzelm
avoid capture of inner/outer context and thus reduce heaps sizes by 20..40% (see also dd04a8b654fc, e49bf4ebf330, 9c19e15c8548, 71467e35fc3c);
2 weeks ago, by wenzelm
proper transfer / trim_context;
2 weeks ago, by wenzelm
more operations "without_context", assuming that the thm has been properly transferred already;
2 weeks ago, by wenzelm
proper trim_context / transfer;
2 weeks ago, by wenzelm
tuned: more accurate check (is_norm_hhf protect);
2 weeks ago, by wenzelm
clarified build options: reduce heap size by approx. 3%;
2 weeks ago, by wenzelm
more standard merge order, following logical structure of imports rather than physical serials;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
proper Thm.trim_context / Thm.transfer;
2 weeks ago, by wenzelm
proper Thm.trim_context / Thm.transfer;
2 weeks ago, by wenzelm
tuned: avoid pointless Proof_Context.init_global of Context.proof_of;
2 weeks ago, by wenzelm
New material from the HOL Light metric space library, mostly about quasi components
2 weeks ago, by paulson
More material from the HOL Light metric space library
2 weeks ago, by paulson
proper Thm.trim_context / Thm.transfer;
2 weeks ago, by wenzelm
proper position for ML-like commands;
2 weeks ago, by wenzelm
more robust: after shutdown;
3 weeks ago, by wenzelm
proper exception CONTEXT for Context.certificate_theory;
3 weeks ago, by wenzelm
more diagnostic operations;
3 weeks ago, by wenzelm
tuned spelling;
3 weeks ago, by wenzelm
more standard treatment of data and context;
3 weeks ago, by wenzelm
more standard val silent = Attrib.setup_config_bool;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
proper Thm.trim_context / Thm.transfer;
3 weeks ago, by wenzelm
proper Thm.trim_context / Thm.transfer;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
tuned Isabelle/ML;
3 weeks ago, by wenzelm
more informative position information;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
more informative position information;
3 weeks ago, by wenzelm
clarified context tracing;
3 weeks ago, by wenzelm
more operations;
3 weeks ago, by wenzelm
proper system options to control context tracing/timing;
3 weeks ago, by wenzelm
added lemmas transp_on_multpHO and transp_multpHO
3 weeks ago, by desharna
tuned theory structure
3 weeks ago, by desharna
merged
3 weeks ago, by desharna
added lemmas Finite_Set.bex_(min|max)_element_with_property and reordered assumptions of Finite_Set.bex_(min|max)_element
3 weeks ago, by desharna
backed out changeset 6c2494750a4e: it hardly makes a difference for heap size, but crashes arm64_32-darwin for unknown reasons;
3 weeks ago, by wenzelm
enforce rebuild of Isabelle/ML + Isabelle/Scala;
3 weeks ago, by wenzelm
updated to jdk-17.0.7;
3 weeks ago, by wenzelm
minor performance tuning (see also f906f7f83dae and b23c42b9f78a);
3 weeks ago, by wenzelm
performance tuning: cached non-persistent Parser.gram reduces heap size by approx. 1-4%;
3 weeks ago, by wenzelm
more operations;
3 weeks ago, by wenzelm
tuned: more readable ML;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
backed out changeset 4660181c83c9: remove rather pointless timing (1..50ms);
3 weeks ago, by wenzelm
maintain dynamic position where values are created (again, amending afa6117bace4);
3 weeks ago, by wenzelm
more robust: publish token only after assignment of result;
3 weeks ago, by wenzelm
tuned comments;
3 weeks ago, by wenzelm
clarified signature;
3 weeks ago, by wenzelm
merged
3 weeks ago, by wenzelm
tuned signature;
3 weeks ago, by wenzelm
support for cached evaluation via weak_ref;
3 weeks ago, by wenzelm
optional timing;
3 weeks ago, by wenzelm
more informative trace of context allocations;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
tuned internal structure;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
tuned whitespace;
3 weeks ago, by wenzelm
merged
3 weeks ago, by desharna
added author
3 weeks ago, by desharna
added lemma asymp_on_multpHO
3 weeks ago, by desharna
added lemmas multpHO_iff_set_mset_lessHO_set_mset and multpHO_minus_inter_minus_inter_iff
3 weeks ago, by desharna
added lemmas count_minus_inter_lt_count_minus_inter_iff and minus_inter_eq_minus_inter_iff
3 weeks ago, by desharna
added lemma multpHO_implies_one_step_strong
3 weeks ago, by desharna
merged
3 weeks ago, by wenzelm
tuned comments;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
hide names more thorougly, in contrast to 1d82061fbb12 and 00e9ca1e7261: e.g. relevant for overlapping accesses seen in 'inductive_set';
3 weeks ago, by wenzelm
minor performance tuning;
3 weeks ago, by wenzelm
minor performance tuning;
3 weeks ago, by wenzelm
back to more elementary concept of aliases as adhoc change of accesses, but now with "suppress" information (see also 31ea5c1f874d);
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
clarified data representation: slightly more compact, since internals_hidden is sparesely populated and rarely changes;
3 weeks ago, by wenzelm
more operations;
3 weeks ago, by wenzelm
more operations;
3 weeks ago, by wenzelm
more operations;
3 weeks ago, by wenzelm
minor performance tuning;
3 weeks ago, by wenzelm
unused;
3 weeks ago, by wenzelm
more complete accesses for "extern" operation, notably for aliases;
3 weeks ago, by wenzelm
more explicit entries for aliases, with proper checks in "strict" mode (e.g. for logical entities);
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
clarified signature;
3 weeks ago, by wenzelm
unused;
3 weeks ago, by wenzelm
minor performance tuning;
3 weeks ago, by wenzelm
tuned signature;
3 weeks ago, by wenzelm
minor performance tuning;
3 weeks ago, by wenzelm
revert pointless performance tuning fd5f4455e033: no measurable difference in HOL, HOL-Library, HOL-Analysis;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
more accurate treatment of traditional name space accesses (refining 948f5dc4d694, fcd85e04a948, 238307775d52);
4 weeks ago, by wenzelm
tuned;
4 weeks ago, by wenzelm
proper treatment of restriction (for 'qualified');
4 weeks ago, by wenzelm
misc tuning;
4 weeks 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;
4 weeks 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;
4 weeks ago, by wenzelm
minor performance tuning: more compact representation of only sparsely table;
4 weeks ago, by wenzelm
minor performance tuning: no storage of accesses, produce Binding.full_name_spec on the spot;
4 weeks ago, by wenzelm
proper checks;
4 weeks ago, by wenzelm
tuned;
4 weeks ago, by wenzelm
tuned structure;
4 weeks ago, by wenzelm
tuned signature;
4 weeks ago, by wenzelm
tuned;
4 weeks ago, by wenzelm
clarified extern vs. alias/hide: output alternative names, if possible;
4 weeks ago, by wenzelm
tuned;
4 weeks ago, by wenzelm
minor performance tuning: more compact, more sharing;
4 weeks ago, by wenzelm
potential performance tuning: more compact data structure, but less sharing;
4 weeks ago, by wenzelm
Importation of additional lemmas from metric.ml
3 weeks ago, by paulson
fixes esp to theory presentation
3 weeks ago, by paulson
new material ported from HOL Light's metric.ml
3 weeks ago, by paulson
merged
4 weeks ago, by paulson
Two new theories containing material ported from HOL Light about abstract topology
4 weeks ago, by paulson
merged
4 weeks ago, by nipkow
streamlined
4 weeks ago, by nipkow
merged
4 weeks ago, by paulson
More new theorems, and a necessary correction
4 weeks ago, by paulson
A few new theorems
4 weeks ago, by paulson
merged
4 weeks ago, by paulson
merged
5 weeks ago, by paulson
merged
7 weeks ago, by paulson
merged
2 months ago, by paulson
Numerous significant simplifications
2 months ago, by paulson
stripped unused functionality
4 weeks ago, by haftmann
tuned
4 weeks ago, by haftmann
case translation in intermediate language eliminates semantic clone
4 weeks ago, by haftmann
minor performance tuning;
4 weeks ago, by wenzelm
more correct type calculation
4 weeks ago, by haftmann
Backed out changeset 5016262a2384
4 weeks ago, by haftmann
added lemma
4 weeks ago, by nipkow
thingol: fix abstraction return types in case
5 weeks ago, by stuebinm
merged
5 weeks ago, by desharna
tuned; avoided intermediate lists
5 weeks ago, by desharna
tuned; avoided intermediate list and list traversal
5 weeks ago, by desharna
tuned; avoided intermediate lists
5 weeks ago, by desharna
tuned; avoided intermediate list
5 weeks ago, by desharna
made 'primcorec' more robust
5 weeks ago, by blanchet
performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
5 weeks ago, by wenzelm
tuned signature;
5 weeks ago, by wenzelm
more operations for lexicographic ordering;
5 weeks ago, by wenzelm
more operations: following Library list operations and Ord_List.T operations;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
tuned: concise combinators instead of bulky case-expressions;
5 weeks ago, by wenzelm
provide ML antiquotation "if_none": non-strict version of "the_default";
5 weeks ago, by wenzelm
merged
5 weeks ago, by wenzelm
proper Thm.trim_context / Thm.transfer (see also 0d401f874942);
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
more operations;
5 weeks ago, by wenzelm
more operations;
5 weeks ago, by wenzelm
more uniform operations wrt. Thm.full_prop_of;
5 weeks ago, by wenzelm
proper Thm.trim_context / Thm.transfer for context data;
5 weeks ago, by wenzelm
tuned: more concise data record;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
clarified counters and types;
5 weeks ago, by wenzelm
tuned signature;
5 weeks ago, by wenzelm
support n-ary merge theory data;
5 weeks ago, by wenzelm
tuned;
6 weeks ago, by wenzelm
tuned;
6 weeks ago, by wenzelm
proper theory_long_name;
6 weeks ago, by wenzelm
prefer theory_long_name in data;
6 weeks ago, by wenzelm
proper theory_long_name;
6 weeks ago, by wenzelm
clarified signature: explicitly distinguish theory_base_name vs. theory_long_name;
6 weeks ago, by wenzelm
tuned;
6 weeks ago, by wenzelm
more operations, following Isabelle/ML conventions;
6 weeks ago, by wenzelm
clarified theory_id: plain value without state;
6 weeks ago, by wenzelm
tuned
6 weeks ago, by haftmann
clarified terminology
6 weeks ago, by haftmann
minor performance tuning: recursive check of pointer_eq;
6 weeks ago, by wenzelm
minor performance tuning: avoid excessive (de)constructions for base cases;
6 weeks ago, by wenzelm
unused (see also 864c7c684651 and b6aa5eac0a1a);
6 weeks ago, by wenzelm
tuned;
6 weeks ago, by wenzelm
tuned;
6 weeks ago, by wenzelm
more operations: avoid intermediate list;
6 weeks ago, by wenzelm
discontinued somewhat pointless operation: Conjunction.intr_balanced / Conjunction.elim_balanced with single hyp performs better (e.g. see AFP/351b7b576892);
6 weeks ago, by wenzelm
update NEWS: Sortset and Termset turned out to be counter productive, Ord_List.union is much lighter;
6 weeks ago, by wenzelm
drop unused Set().ord, which is potentially inefficient due to dict_ord/dest;
6 weeks ago, by wenzelm
tuned;
6 weeks ago, by wenzelm
backout b6aa5eac0a1a;
6 weeks ago, by wenzelm
tuned;
6 weeks ago, by wenzelm
Thm.shared context: speed-up low-level inferences;
6 weeks ago, by wenzelm
tuned whitespace;
6 weeks ago, by wenzelm
backout 4a174bea55e2;
6 weeks ago, by wenzelm
Backed out changeset f34d11942ac1
6 weeks ago, by wenzelm
backout e3fe192fa4a8;
6 weeks ago, by wenzelm
backout 61f652dd955a;
6 weeks ago, by wenzelm
Backed out changeset e3db27e3b0c6
6 weeks ago, by wenzelm
Backed out changeset cd5d56abda10
6 weeks ago, by wenzelm
revert b43ee37926a9 due to problems with AFP/PAPP_Impossibility;
6 weeks ago, by wenzelm
merged
6 weeks ago, by wenzelm
tuned;
6 weeks ago, by wenzelm
merged
6 weeks ago, by Lars Hupel
code_target: create subdirectories for export_code file
8 weeks ago, by stuebinm
clarified signature: support "suppress" prefix as int, followed by list;
6 weeks ago, by wenzelm
minor performance tuning: more elementary operations;
6 weeks ago, by wenzelm
tuned signature;
6 weeks ago, by wenzelm
minor performance tuning: more elementary operations;
6 weeks ago, by wenzelm
tuned signature;
6 weeks ago, by wenzelm
more operations;
6 weeks ago, by wenzelm
more direct hg_sync init via ssh (see also 721b3278c8e4);
6 weeks ago, by wenzelm
tuned;
6 weeks ago, by wenzelm
more operations;
6 weeks ago, by wenzelm
tuned: more direct re-use;
6 weeks ago, by wenzelm
more direct clone (see also change of exception in 8d8c70b41bab);
6 weeks ago, by wenzelm
more operations, following Isabelle/ML conventions;
6 weeks ago, by wenzelm
more operations, following Isabelle/ML conventions;
6 weeks ago, by wenzelm
proforma use of Long_Name.chunks, without change of the representation of accesses yet;
6 weeks ago, by wenzelm
merged
6 weeks ago, by wenzelm
minor performance tuning;
6 weeks ago, by wenzelm
compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
6 weeks ago, by wenzelm
clarified signature;
6 weeks ago, by wenzelm
misc tuning and clarification;
7 weeks ago, by wenzelm
more compact: avoid redundant entries;
7 weeks ago, by wenzelm
tuned;
7 weeks ago, by wenzelm
tuned;
7 weeks ago, by wenzelm
more operations;
7 weeks ago, by wenzelm
performance tuning: proper pointer_eq;
7 weeks ago, by wenzelm
added lemmas multpHO_repeat_mset_repeat_mset[simp] and multpHO_double_double[simp]
7 weeks ago, by desharna
merged
7 weeks ago, by desharna
added lemma multp_image_mset_image_msetI
7 weeks ago, by desharna
merged
7 weeks ago, by nipkow
proper invariants
7 weeks ago, by nipkow
merged
7 weeks ago, by wenzelm
misc tuning: follow Table() more closely;
7 weeks ago, by wenzelm
tuned signature;
7 weeks ago, by wenzelm
tuned;
7 weeks ago, by wenzelm
performance tuning: replace Ord_List by Table();
7 weeks ago, by wenzelm
performance tuning: replace Ord_List by Set();
7 weeks ago, by wenzelm
tuned;
7 weeks ago, by wenzelm
more operations;
7 weeks ago, by wenzelm
tuned;
7 weeks ago, by wenzelm
performance tuning: replace Table() by Set();
7 weeks ago, by wenzelm
minor performance tuning: more compact persistent data;
7 weeks ago, by wenzelm
performance tuning: replace Table() by Set();
7 weeks ago, by wenzelm
tuned;
7 weeks ago, by wenzelm
more operations;
7 weeks ago, by wenzelm
unused (see 34dd96a06c45);
7 weeks ago, by wenzelm
more compact data: approx. 75% .. 85% of AList size;
7 weeks ago, by wenzelm
tuned;
7 weeks ago, by wenzelm
some remarks on division
7 weeks ago, by haftmann
proper section headings
7 weeks ago, by haftmann
more NEWS;
7 weeks ago, by wenzelm
clarified NEWS;
7 weeks ago, by wenzelm
performance tuning: replace Ord_List by Set();
7 weeks ago, by wenzelm
tuned;
7 weeks ago, by wenzelm
performance tuning: replace Ord_List by Table();
7 weeks ago, by wenzelm
more Set() and Table() instances;
7 weeks ago, by wenzelm
tuned;
7 weeks ago, by wenzelm
performance tuning: replace Ord_List by Set();
7 weeks ago, by wenzelm
performance tuning: make_size accounts for boxes, i.e. pointer derefs required in "count";
7 weeks ago, by wenzelm
NEWS;
7 weeks ago, by wenzelm
performance tuning;
7 weeks ago, by wenzelm
more robust: avoid crash of Build_Log.parse_build_info / Protocol.Error_Message_Marker, e.g. in session MDP-Rewards of Isabelle/26ec258e5cf8 + AFP/2859e11cc09b;
7 weeks ago, by wenzelm
proper stmt.execute() within loop (amending 9d9b30741fc4);
7 weeks ago, by wenzelm
clarified signature;
7 weeks ago, by wenzelm
tuned comments;
7 weeks ago, by wenzelm
more options;
7 weeks ago, by wenzelm
removed obsolete "rsync" package;
7 weeks ago, by wenzelm
tuned comments;
7 weeks ago, by wenzelm
use "rsync --secluded-args" by default, discontinue obsolete option -P of sync tools;
7 weeks ago, by wenzelm
tuned output;
7 weeks ago, by wenzelm
misc tuning and clarification;
7 weeks ago, by wenzelm
clarified output;
7 weeks ago, by wenzelm
use remote copy of locally installed rsync component: for uniform version and options;
7 weeks ago, by wenzelm
clarified signature: more abstract;
7 weeks ago, by wenzelm
tuned signature;
7 weeks ago, by wenzelm
more direct Hg_Sync.check_directory via SSH operations;
7 weeks ago, by wenzelm
tuned;
7 weeks ago, by wenzelm
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
7 weeks ago, by wenzelm
clarified signature: avoid object-oriented "dispatch";
7 weeks ago, by wenzelm
tuned;
8 weeks ago, by wenzelm
clarified signature: more uniform Table() vs. Set();
8 weeks ago, by wenzelm
merged
2 months ago, by wenzelm
clarified modules;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
more compact data;
2 months ago, by wenzelm
minor performance tuning;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
more uniform treatment of properties (but < 0 should not occur here);
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
misc tuning and clarification: more tight representation;
2 months ago, by wenzelm
tuned: prefer "build" combinator;
2 months ago, by wenzelm
tuned
2 months ago, by nipkow
tuned signature;
2 months ago, by wenzelm
more operations for profiling;
2 months ago, by wenzelm
provide rsync component, with uniform version + options on all platforms;
2 months ago, by wenzelm
tuned message;
2 months ago, by wenzelm
provide local component to remote directory;
2 months ago, by wenzelm
tuned output;
2 months ago, by wenzelm
more SSH operations;
2 months ago, by wenzelm
more operations;
2 months ago, by wenzelm
tuned comments;
2 months ago, by wenzelm
clarified directory names, following bash_process (see e59d7d6fe1bd);
2 months ago, by wenzelm
tuned README;
2 months ago, by wenzelm
clarified build options;
2 months ago, by wenzelm
more portable options;
2 months ago, by wenzelm
build rsync from sources, to avoid divergence of protocols on various platforms;
2 months ago, by wenzelm
more informative errors;
2 months ago, by wenzelm
clarified options;
2 months ago, by wenzelm
tuned messages;
2 months ago, by wenzelm
provide Isabelle tool wrapper;
2 months ago, by wenzelm
more robust errors: proceed updating database;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned output;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
clarified modules;
2 months ago, by wenzelm
tuned comments (amending 1951f6470792);
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
discontinue somewhat pointless is_single, which also depends on details of internal data representation;
2 months ago, by wenzelm
more compact data: approx. 0.85 .. 1.10 of plain list size;
2 months ago, by wenzelm
slightly more compact data;
2 months ago, by wenzelm
more operations, notably for profiling;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
more compact representation of leaf nodes: only 1.10 .. 1.33 larger than plain list;
2 months ago, by wenzelm
tuned --- fewer compiler warnings;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned signature: more uniform structure Key;
2 months ago, by wenzelm
prefer Sortset.T for shyps;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
more operations;
2 months ago, by wenzelm
tuned names: "e" means "entry" in table.ML and "elem" in set.ML;
2 months ago, by wenzelm
NEWS;
2 months ago, by wenzelm
added Set.size;
2 months ago, by wenzelm
performanc tuning: avoid exception overhead, potentially relevant for Sorts.class_less;
2 months ago, by wenzelm
performance tuning: prefer functor Set() over Table();
2 months ago, by wenzelm
efficient representation of sets: more compact than Table.set;
2 months ago, by wenzelm
tuned whitespace;
2 months ago, by wenzelm
tuned comments;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
tuned output;
2 months ago, by wenzelm
removed junk (amending 236e43c8bb5b);
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned output;
2 months ago, by wenzelm
tuned performance: much faster low-level operation;
2 months ago, by wenzelm
clarified signature: more general operation Bytes.read_slice;
2 months ago, by wenzelm
clarified signature: more explicit types;
2 months ago, by wenzelm
clarified signature: more explicit types;
2 months ago, by wenzelm
clarified signature: more explicit types;
2 months ago, by wenzelm
More explicit type information in dictionary arguments.
2 months ago, by haftmann
tuned
2 months ago, by haftmann
tuned whitespace
2 months ago, by haftmann
more uniform approach towards satisfied applications
2 months ago, by haftmann
more uniform approach towards satisfied applications
2 months ago, by haftmann
tuned
2 months ago, by haftmann
tuned
2 months ago, by haftmann
Tuned semicolons.
2 months ago, by haftmann
reordered assumption and tuned proof of Multiset.bex_least_element and Multiset.bex_greatest_element
2 months ago, by desharna
added lemmas Finite_Set.bex_least_element and Finite_Set.bex_greatest_element
2 months ago, by desharna
refactored proofs
2 months ago, by desharna
added lemmas Finite_Set.bex_min_element and Finite_Set.bex_max_element
2 months ago, by desharna
reversed import dependency between Relation and Finite_Set; and move theorems around
2 months ago, by desharna
more operations;
2 months ago, by wenzelm
clarified theory_sizeof1_data: count bytes, individually for each data entry;
2 months ago, by wenzelm
clarified operations for ML object sizes;
2 months ago, by wenzelm
merged
2 months ago, by paulson
simplified a lot of messy proofs
2 months ago, by paulson
merged
2 months ago, by desharna
added lemma multp_repeat_mset_repeat_msetI
2 months ago, by desharna
more operations;
2 months ago, by wenzelm
merged
2 months ago, by paulson
merged
2 months ago, by paulson
Proof simplification
2 months ago, by paulson
proper "build_thorough" for "isabelle update" (amending 9e5f8f6e58a0);
2 months ago, by wenzelm
merged
2 months ago, by wenzelm
back to compression in Isabelle/Scala (in contrast to f7174238b5e3), e.g. relevant for old_command_timings_blob, but also for prospective heaps;
2 months ago, by wenzelm
vacuum everything in the database;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
proper vacuum of session_info tables: only once per build process;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
more thorough database checks;
2 months ago, by wenzelm
more thorough treatment of build prefs, guarded by system option "build_through": avoid accidental rebuild of HOL etc.;
2 months ago, by wenzelm
clarified build options;
2 months ago, by wenzelm
clarified ML option vs. Scala option (see also caa182bdab7a);
2 months ago, by wenzelm
merge conflict
2 months ago, by nipkow
unified function update and map update syntaxes
2 months ago, by nipkow
removed accidental junk
2 months ago, by blanchet
map update syntax
2 months ago, by nipkow
proper sorting of result (amending f458547b4f0f);
2 months ago, by wenzelm
merged
2 months ago, by wenzelm
enforce rebuild of Isabelle/ML;
2 months ago, by wenzelm
more operations;
2 months ago, by wenzelm
more specific vacuum operation, which is also relevant to PostgreSQL;
2 months ago, by wenzelm
tuned signature: removed redundant argument;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
proper build_uuid for Build_Process.Task: thus old entries are removed via prepare_database/clean_build;
2 months ago, by wenzelm
more informative Build_Process.Snapshot;
2 months ago, by wenzelm
more explicit snapshot of "_state" and "_database";
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
removed redundant State.workers: directly maintained within the database, using with SQL update;
2 months ago, by wenzelm
more thorough cleanup;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
more thorough synchronization of internal "_state" vs. external "_database";
2 months ago, by wenzelm
more database content;
2 months ago, by wenzelm
clarified modules;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
clarified modules;
2 months ago, by wenzelm
tuned output;
2 months ago, by wenzelm
tuned output;
2 months ago, by wenzelm
Adjusted to new map update priorities
2 months ago, by nipkow
bring priority in line with ordinary function update notation
2 months ago, by nipkow
merged
2 months ago, by nipkow
use tree (simpler) instead of rbt (exercise)
2 months ago, by nipkow
enforce rebuild of Isabelle/ML;
2 months ago, by wenzelm
more direct state update;
2 months ago, by wenzelm
avoid too many synchronized_database;
2 months ago, by wenzelm
tuned output;
2 months ago, by wenzelm
synchronize progress messages with database;
2 months ago, by wenzelm
more robust SQL query for mandatory arguments;
2 months ago, by wenzelm
synchronize progress stop/stopped with database;
2 months ago, by wenzelm
more database content;
2 months ago, by wenzelm
tuned whitespace;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
tuned whitespace;
2 months ago, by wenzelm
clarified signature: avoid confusion due to object-orientation;
2 months ago, by wenzelm
clarified modules;
2 months ago, by wenzelm
clarified signature: prefer explicit types;
2 months ago, by wenzelm
more accurate Sessions.Info.session_prefs: cover relative changes wrt. statically declared options;
2 months ago, by wenzelm
clarified signature: more explicit type Options.Spec, which incorporates all variants of Options.+;
2 months ago, by wenzelm
tuned output;
2 months ago, by wenzelm
clarified signature: more explicit types;
2 months ago, by wenzelm
clarified signature: prefer static types;
2 months ago, by wenzelm
clarified signature (again, see also 8c64e51d9dde and 268bf61631ec);
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
more operations, thanks to Jsoup;
2 months ago, by wenzelm
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
2 months ago, by wenzelm
more accurate shasum_meta_info;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
support "isabelle options -l -t TAGS";
2 months ago, by wenzelm
NEWS;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
avoid hard-wired stuff (see also 78f2475aa126);
2 months ago, by wenzelm
clarified tags;
2 months ago, by wenzelm
clarified session prefs (or "options" within the database);
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
tuned comments;
2 months ago, by wenzelm
unused (see 268bf61631ec);
2 months ago, by wenzelm
clarified exported options;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
do not export connection details (password etc.);
2 months ago, by wenzelm
support option tags;
2 months ago, by wenzelm
use simplifier to classify the missing assumptions in Sledgehammer's abduction mechanism
2 months ago, by blanchet
don't try to falisfy goals with schematics
2 months ago, by blanchet
enforce rebuild of Isabelle/ML;
2 months ago, by wenzelm
more robust transactions;
2 months ago, by wenzelm
proper support for Option[Date] columns;
2 months ago, by wenzelm
more robust transactions;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
enforce rebuild of Isabelle/ML;
2 months ago, by wenzelm
proper test (amending 32f9e75c92e9);
2 months ago, by wenzelm
updated to sqlite-jdbc-3.41.0.0;
2 months ago, by wenzelm
proper shasum lines (amending 3070001c9d1f);
2 months ago, by wenzelm
more robust transactions;
2 months ago, by wenzelm
explicit locking for PostgreSQL --- neither available nor required for SQLite;
2 months ago, by wenzelm
merged
2 months ago, by wenzelm
assume total operation: ProcessHandle.current().info.startInstant appears to work on all platforms;
2 months ago, by wenzelm
more database content, e.g. for monitoring;
2 months ago, by wenzelm
tuned structure;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
more database content, e.g. for monitoring;
2 months ago, by wenzelm
more explicit workers, e.g. for monitoring;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
clarified worker state: always maintain database content via worker_uuid;
2 months ago, by wenzelm
clarified signature: prefer Build_Process.Context for parameters;
2 months ago, by wenzelm
support for "isabelle build -j0": require external workers to make progress;
2 months ago, by wenzelm
follow renaming of various Isabelle command-line tools (see b975f5aaf6b8 and before);
2 months ago, by wenzelm
require the presence of free variables to do abduction in Sledgehammer
2 months ago, by blanchet
removed exercise solution
2 months ago, by nipkow
merged
2 months ago, by nipkow
new theory Tree_Rotations
2 months ago, by nipkow
proper tool name (amending cbb49fe8e5a2);
2 months ago, by wenzelm
proper file-name (amending b975f5aaf6b8);
2 months ago, by wenzelm
tuned headers;
2 months ago, by wenzelm
eliminated suspicious Unicode characters;
2 months ago, by wenzelm
tuned whitespace;
2 months ago, by wenzelm
renamed "isabelle build_docker" to "isabelle docker_build" (unrelated to "isabelle build");
2 months ago, by wenzelm
renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
2 months ago, by wenzelm
renamed "isabelle build_components" to "isabelle components_build" (unrelated to "isabelle build");
2 months ago, by wenzelm
sort lines;
2 months ago, by wenzelm
renamed "isabelle log" to "isabelle build_log";
2 months ago, by wenzelm
clarified structure;
2 months ago, by wenzelm
tuned output;
2 months ago, by wenzelm
clarified signature: proper abstract type;
2 months ago, by wenzelm
clarified signature: support all arguments of Sessions.store();
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
basic setup for "isabelle build_worker";
2 months ago, by wenzelm
tuned comments;
2 months ago, by wenzelm
tuned structure;
2 months ago, by wenzelm
clarified terminology of "session build database", while "build database" is the one underlying Build_Process;
2 months ago, by wenzelm
clarified modules;
2 months ago, by wenzelm
clarified signature: reduce boilerplate;
2 months ago, by wenzelm
clarified messages;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
tuned structure;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
clarified build process roles: "worker" vs. "build";
2 months ago, by wenzelm
clarified database content;
2 months ago, by wenzelm
tuned: prefer iterator.nextOption;
2 months ago, by wenzelm
tuned whitespace and braces;
2 months ago, by wenzelm
clarified signature: more uniform operations;
2 months ago, by wenzelm
tuned signature: reduce boilerplate;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
proper clean_build of old data at start of new process --- allow to inspect remains of the last process;
2 months ago, by wenzelm
more database content: formal end_build;
2 months ago, by wenzelm
more operations;
2 months ago, by wenzelm
clarified database content and prepare/init stages;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
less verbosity, amending 3bc49507bae5;
2 months ago, by wenzelm
tuned comments;
2 months ago, by wenzelm
tuned signature: avoid totally adhoc overriding;
2 months ago, by wenzelm
separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
2 months ago, by wenzelm
enforce rebuild of Isabelle/ML, after various changes to build database management;
2 months ago, by wenzelm
more detailed table "isabelle_build_serial": allow to monitor activity of build_process instances;
2 months ago, by wenzelm
tuned output;
2 months ago, by wenzelm
clarified database content: store actual value instead of index;
2 months ago, by wenzelm
more robust: disallow override;
2 months ago, by wenzelm
tuned messages;
2 months ago, by wenzelm
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
2 months ago, by wenzelm
clarified signature: manage "verbose" flag via "progress";
2 months ago, by wenzelm
removed unused arguments: avoid ambiguity concerning progress/verbose;
2 months ago, by wenzelm
clarified protocol for "verbose" messages;
2 months ago, by wenzelm
clarified signature: manage "verbose" flag via "progress";
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
more operations;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
more robust: proper bound checks;
2 months ago, by wenzelm
enforce rebuild of Isabelle/ML, after various changes to build database management;
2 months ago, by wenzelm
clarified modules;
2 months ago, by wenzelm
clarified signature: manage "verbose" flag via "progress";
2 months ago, by wenzelm
clarified treatment of "verbose" messages, e.g. Progress.theory();
2 months ago, by wenzelm
proper "val verbose" (amending 2e2b2bd6b2d2);
2 months ago, by wenzelm
tuned whitespace;
2 months ago, by wenzelm
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
2 months ago, by wenzelm
support progress backed by database;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned messages;
2 months ago, by wenzelm
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
2 months ago, by wenzelm
proper Output.writeln_text (with clean_yxml) for all instances of Progress.echo;
2 months ago, by wenzelm
merged
2 months ago, by wenzelm
more database content;
2 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned whitespace;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
merged
3 months ago, by paulson
More of Eberl's material
3 months ago, by paulson
Some new lemmas. Some tidying up
3 months ago, by paulson
detect duplicates in Sledgehammer output -- suggested by Larry Paulson
3 months ago, by blanchet
got rid of 'important message' mechanism in SystemOnTPTP (which is less used nowadays)
3 months ago, by blanchet
merged
3 months ago, by wenzelm
clarified execution context: main work happens within Future.thread;
3 months ago, by wenzelm
clarified timeout: closer to actual process;
3 months ago, by wenzelm
tuned names;
3 months ago, by wenzelm
clarified names;
3 months ago, by wenzelm
tuned, following ML_Statistics.monitor;
3 months ago, by wenzelm
unused (see also 0cebcbeac4c7);
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned comments;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more robust: proper synchronization of transition from next_job to start_session;
3 months ago, by wenzelm
more thorough synchronized_database for internal *and* external state;
3 months ago, by wenzelm
simplified startup under "locked" condition (in contrast to f7e413e8d269);
3 months ago, by wenzelm
more explicit session name, in anticipation of variants like "session.document", "session.browser_info";
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned signature: support general Build_Job instances;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
clarified signature: prefer static data;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
unused;
3 months ago, by wenzelm
tuned signature (again);
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
proper deps from build_graph, not imports_graph (amending 0c704aba71e3);
3 months ago, by wenzelm
misc tuning: more direct access to ancestors, without build_graph;
3 months ago, by wenzelm
tuned signature (again);
3 months ago, by wenzelm
clarified signature: reduce explicit access to static Sessions.Structure;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
clarified modules (again);
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
avoid premature Properties.uncompress: allow blob to be stored in another database;
3 months ago, by wenzelm
more robust: synchronized access to database;
3 months ago, by wenzelm
clarified signature: do not expose global state to object-oriented variants;
3 months ago, by wenzelm
tuned comments and outline;
3 months ago, by wenzelm
merged
3 months ago, by paulson
Imported a theorem about Infinite_Sum. Importing this theory a bit earlier is causing syntactic ambiguities with Infinite_Set_Sum however; no_notation needed
3 months ago, by paulson
A little bit more tidying up
3 months ago, by paulson
tweaked Sledgehammer interaction
3 months ago, by blanchet
there won't be an E version 2.7
3 months ago, by blanchet
reverted 0506c3273814 -- the message is still useful
3 months ago, by blanchet
compile
3 months ago, by blanchet
adopt terminology suggested by Larry Paulson
3 months ago, by blanchet
more robust E proof parsing
3 months ago, by blanchet
avoid double 'Warning:' in Sledgehammer messages
3 months ago, by blanchet
tweaked abduction in Sledgehammer
3 months ago, by blanchet
slightly more documentation
3 months ago, by blanchet
renamed new Sledgehammer option
3 months ago, by blanchet
updated documentation
3 months ago, by blanchet
improve ad hoc abduction in Sledgehammer
3 months ago, by blanchet
tuning
3 months ago, by blanchet
don't apply abduction and consistency checking to goals of the form 'False'
3 months ago, by blanchet
implemented ad hoc abduction in Sledgehammer with E
3 months ago, by blanchet
tuned;
3 months ago, by wenzelm
clarified scope of "serial" and "numa_index" within database;
3 months ago, by wenzelm
clarified signature: allow more general init, e.g. from existing database;
3 months ago, by wenzelm
clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
simplified somewhat pointless error message (see also 0189fe0f6452);
3 months ago, by wenzelm
clafified signature: simplify object-oriented reuse;
3 months ago, by wenzelm
revert pointless 375c6b9ce9ea: overall thread context is already uninterruptible (see 54ac957c53ec);
3 months ago, by wenzelm
tuned whitespace;
3 months ago, by wenzelm
merged
3 months ago, by paulson
Fixed a presentation error
3 months ago, by paulson
Importation of basic group theory results, due to Jakob von Raumer from his AFP entry Jordan-Hölder Theorem
3 months ago, by paulson
tuned whitespace;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified signature, although "sql" argument is de-facto mandatory;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
proper SQL (amending 7ab9bac1ca96);
3 months ago, by wenzelm
clarified signature: more explicit "synchronized" regions;
3 months ago, by wenzelm
more robust interrupt handling, notably for Build_Job.terminate();
3 months ago, by wenzelm
clarified signature: works for general Build_Job;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
proper log_lines, without protocol messages (amending cb3f5361fbca);
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
tuned messages;
3 months ago, by wenzelm
clarified error output vs. process_result stored in build_database (see also 13a0f537e232 and bff56eae3ec5);
3 months ago, by wenzelm
clarified system option: guard for testing, until the database layout has stabilized;
3 months ago, by wenzelm
merged
3 months ago, by paulson
Simplified some proofs
3 months ago, by paulson
clarified db content: avoid redundancy of historic ML_IDENTIFIER;
3 months ago, by wenzelm
merged
3 months ago, by wenzelm
proper filterNot, not filterNot-not;
3 months ago, by wenzelm
option build_hostname allows to change hostname easily;
3 months ago, by wenzelm
clarified permissions of build.db, following server.db;
3 months ago, by wenzelm
enforce rebuild of Isabelle/ML, after various changes to build database management;
3 months ago, by wenzelm
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
3 months ago, by wenzelm
tuned: fewer warnings in IntelliJ IDEA;
3 months ago, by wenzelm
clarified init_database vs. update_database: implicitly assume fresh "instance";
3 months ago, by wenzelm
clarified Build_Process.Context: cover all static information;
3 months ago, by wenzelm
tuned whitespace in generated SQL;
3 months ago, by wenzelm
tuned: prefer typed operations;
3 months ago, by wenzelm
clarified signature: more concise operations;
3 months ago, by wenzelm
more robust options in "prefs" format: avoid odd control character;
3 months ago, by wenzelm
proper settings for hostname: allow to adjust it in user space;
3 months ago, by wenzelm
support for build database: still inactive;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
clarified signature: more robust operations;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more operations;
3 months ago, by wenzelm
clarified signature: more operations;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
clarified signature: more robust (see also cf2ef4be3630);
3 months ago, by wenzelm
unused (see also 7b318273a4aa and a1fb4d28e609);
3 months ago, by wenzelm
tidying ugly proofs
3 months ago, by paulson
brought back [...] maplet syntax
3 months ago, by nipkow
merged
3 months ago, by paulson
has_sum now an infix operator!!
3 months ago, by paulson
merged
3 months ago, by paulson
New material contributed by Manuel
3 months ago, by paulson
Map.empty no longer output abbreviation; %_. None is shorter and requires no explanation
3 months ago, by nipkow
added lemmas strict_subset_implies_multpDM and strict_subset_implies_multpHO
3 months ago, by desharna
added lemma multpDM_plus_plusI[simp]
3 months ago, by desharna
added lemmas multpDM_mono_strong and multpHO_mono_strong
3 months ago, by desharna
merged
3 months ago, by paulson
One new (necessary) theorem
3 months ago, by paulson
merged
3 months ago, by wenzelm
more operations to support management of jobs, e.g. from external database;
3 months ago, by wenzelm
more uniform operations;
3 months ago, by wenzelm
more operations;
3 months ago, by wenzelm
clarified signature: more robust;
3 months ago, by wenzelm
more operations;
3 months ago, by wenzelm
allow arbitrary info, e.g. for custom scheduler;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
merged
3 months ago, by paulson
Simplified some proofs
3 months ago, by paulson
merged
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned signature: avoid warnings in IntelliJ IDEA;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
clarified state: more explicit type as plain value, which is also easier to sync with external db;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
clarified signature: support meaningful subclasses for Build.Engine implementations;
3 months ago, by wenzelm
support alternative build engines, via system option "build_engine";
3 months ago, by wenzelm
misc tuning and clarification;
3 months ago, by wenzelm
proper test, following Platform.is_linux;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
merged
3 months ago, by paulson
Simplified some more proofs
3 months ago, by paulson
merged
3 months ago, by paulson
Replacing z powr of_int i by z powi i and adding new material from the AFP
3 months ago, by paulson
merged
3 months ago, by wenzelm
tuned: avoid redundant white space;
3 months ago, by wenzelm
clarified signature: more robust operations, without assumption about node 0;
3 months ago, by wenzelm
clarified signature: more concise operations;
3 months ago, by wenzelm
clarified modules: NUMA is managed by Build_Process;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
clarified signature: move all parameters into Build_Process.Context;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
more elementary data structures, to fit better to SQL database;
3 months ago, by wenzelm
clarified signature (see also 68a7ad1385bc);
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
merged
3 months ago, by nipkow
merge in backouts
3 months ago, by nipkow
Backed out changeset bafdc56654cf
3 months ago, by nipkow
backout rev 334015f9098e (for Main_Doc.thy only)
3 months ago, by nipkow
Backed out changeset 1fde0e4fd791
3 months ago, by nipkow
merged
3 months ago, by paulson
Simplifying more proofs
3 months ago, by paulson
merged
3 months ago, by wenzelm
proper Nodes.init (amending 9b35c1171d9a);
3 months ago, by wenzelm
unused;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified signature defaults;
3 months ago, by wenzelm
clarified types: support a variety of Build_Job instances;
3 months ago, by wenzelm
clarified signature: more explicit synchronized operations;
3 months ago, by wenzelm
clarified signature: more explicit synchronized operations;
3 months ago, by wenzelm
clarified modules (again);
3 months ago, by wenzelm
clarified signature: more explicit synchronized operations;
3 months ago, by wenzelm
clarified signature: more explicit synchronized operations;
3 months ago, by wenzelm
more robust: first register job, then start job;
3 months ago, by wenzelm
clarified signature: proper scope of synchronized operation;
3 months ago, by wenzelm
proper synchronized access to mutable state, to support concurrency eventually;
3 months ago, by wenzelm
tuned signature: explicit marker for mutable global state;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more robust;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
merged
3 months ago, by paulson
Tidied some really messy proofs
3 months ago, by paulson
added lemmas asymp_not_liftable_to_multpHO and asymp_multpHO
3 months ago, by desharna
Simplified a few proofs
3 months ago, by paulson
Moved up a theorem
3 months ago, by paulson
Limit properties for complex exponential
3 months ago, by paulson
More of Eberl's contributions: memomorphic functions
3 months ago, by paulson
merged
3 months ago, by paulson
New material due to Eberl on Formal Laurent Series
3 months ago, by paulson
merged
3 months ago, by paulson
A bit more tidying and some new material
3 months ago, by paulson
removed rarely used error in Sledgehammer
3 months ago, by blanchet
merged
3 months ago, by nipkow
tuned
3 months ago, by nipkow
added refute mode to Sledgehammer to find 'counterexamples'
3 months ago, by blanchet
merged
3 months ago, by nipkow
Map.map_of movement
3 months ago, by nipkow
removed Map from docu
3 months ago, by nipkow
move map_of to List
3 months ago, by nipkow
updated NEWS
3 months ago, by blanchet
careful eta-contraction in Metis to keep argument to All and Ex expanded
3 months ago, by blanchet
merged
3 months ago, by wenzelm
merged
3 months ago, by wenzelm
clarified main operations;
3 months ago, by wenzelm
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
3 months ago, by wenzelm
prefer global mutable state, in order to break up the loop eventually;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
clarified static build_context vs. dynamic queue;
3 months ago, by wenzelm
clarified signature: make dynamic Queue from static Context;
3 months ago, by wenzelm
clarified data structure: absorb Option[Process_Result] into Process_Result, e.g. to simplify database storage;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified data structure: use static info from deps, not dynamic results;
3 months ago, by wenzelm
clarified data structure: more direct access to timeout;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
misc tuning and clarification;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
tuned message: old_time not sufficiently prominent nor accurate to be printed;
3 months ago, by wenzelm
clarified signature and terminology;
3 months ago, by wenzelm
clarified signature: avoid adhoc constants;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned message;
3 months ago, by wenzelm
tuned signature: more operations;
3 months ago, by wenzelm
clarified signature: more explicit types;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
merged
3 months ago, by paulson
Simplification of proofs
3 months ago, by paulson
explicit range types in abstractions
3 months ago, by stuebinm
somehow more clear terminology
3 months ago, by haftmann
tuned
3 months ago, by haftmann
Some basis results about trigonometric functions
3 months ago, by paulson
merged
3 months ago, by paulson
Even more new material from Eberl and Li
3 months ago, by paulson
merged
3 months ago, by paulson
More material for Analysis and Complex_Analysis
3 months ago, by paulson
actually executable enum_all, enum_ex for word
3 months ago, by haftmann
tuned text
3 months ago, by nipkow
Lots of new material chiefly about complex analysis
3 months ago, by paulson
merged
3 months ago, by paulson
More new theorems from the number theory development
3 months ago, by paulson
merged
3 months ago, by wenzelm
proper orientation for right-associative operations;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
obsolete --- superseded by SHA1.Shasum operations;
3 months ago, by wenzelm
clarified signature, using right-associative operation;
3 months ago, by wenzelm
tuned whitespace;
3 months ago, by wenzelm
tuned --- implicit split;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
prefer explicit shasum: more robust due to explicit file names, which often work implicitly in LaTeX;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
more uniform use of SHA1.Shasum;
3 months ago, by wenzelm
proper Shasum.digest, to emulate old form from build_history database;
3 months ago, by wenzelm
prefer explicit shasum;
3 months ago, by wenzelm
proper symbolic dependencies, e.g. for Demo_FoilTeX;
3 months ago, by wenzelm
prefer explicit shasum;
3 months ago, by wenzelm
clarified signature: follow terminology of isabelle.Sessions and isabelle.Build;
3 months ago, by wenzelm
clarified signature: follow terminology of isabelle.Sessions and isabelle.Build;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
Some more new material and some tidying of existing proofs
3 months ago, by paulson
more diagnostic operations (see also 5c7652e9bc01);
3 months ago, by wenzelm
more thorough consolidation: follow dependencies of forked proofs (e.g. see theories MaxPrefix vs. MaxChop in AFP/Functional-Automata);
3 months ago, by wenzelm
clarified signature selection: SortedSet[String], which fits better to stored json and works properly on Windows (NB: document theories have an authentic session-theory name);
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
update to polyml-5e9c8155ea96, which is more robust on arm64;
3 months ago, by wenzelm
more robust dependencies for Pure;
3 months ago, by wenzelm
proper compiler root for arm64;
3 months ago, by wenzelm
clarified "isabelle build_polyml": download and build everything for current platform;
3 months ago, by wenzelm
no view_document after build: avoid loss of focus, especially in "auto build" mode;
3 months ago, by wenzelm
tuned message;
3 months ago, by wenzelm
build only if required, view only after proper build: thus avoid pointless events in "auto build" mode;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
maintain document_output meta data;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
avoid redundant SelectionChanged events;
3 months ago, by wenzelm
more logging;
3 months ago, by wenzelm
proper symbolic handle on component resources:
3 months ago, by wenzelm
more robust on Windows, where C:\\ and \\SERVER\SHARE cause problems (line 920 of winbasicio.cpp);
3 months ago, by wenzelm
More of Manuel's material, and some changes
3 months ago, by paulson
less verbosity by default, notably for regular "isabelle build -o document";
3 months ago, by wenzelm
clarified message: old-style log is usually empty;
3 months ago, by wenzelm
clarified messages, notably for session "Intro";
3 months ago, by wenzelm
merged
3 months ago, by wenzelm
more general program start message;
3 months ago, by wenzelm
clarified terminology of inlined "PROGRAM START" messages;
3 months ago, by wenzelm
isabelle update -u cite -l "";
3 months ago, by wenzelm
less ambitious parallelism: avoid exhaustion of memory (40GB total);
3 months ago, by wenzelm
clarified GUI;
4 months ago, by wenzelm
clarified GUI: omit pointless search buttons, as real output is shown as markup;
4 months ago, by wenzelm
more uniform use of Symbol.output, even in situations where its Symbol.encode is usually redundant;
4 months ago, by wenzelm
merged
4 months ago, by paulson
More new material thanks to Manuel
4 months ago, by paulson
merged
4 months ago, by nipkow
tuning
4 months ago, by nipkow
alternate AFP tests on lrzcloud2, to fit better into one day;
4 months ago, by wenzelm
merged
4 months ago, by wenzelm
support document preparation from already loaded theories;
4 months ago, by wenzelm
clarified GUI events;
4 months ago, by wenzelm
clarified GUIs: keep related buttons together;
4 months ago, by wenzelm
proper program name, e.g. for session "Intro";
4 months ago, by wenzelm
clarified GUI events: reset everything on session context switch;
4 months ago, by wenzelm
clarified GUI events: ensure fresh output when switching pages;
4 months ago, by wenzelm
clarified GUI: avoid odd jumping pages on "Cancel";
4 months ago, by wenzelm
clarified GUI events;
4 months ago, by wenzelm
more accurate output: avoid output_body from last run;
4 months ago, by wenzelm
more accurate output: avoid output_main from last run;
4 months ago, by wenzelm
removed unused operation from 3f50b24909df;
4 months ago, by wenzelm
clarified guard: avoid spurious auto builds;
4 months ago, by wenzelm
automatically build document when selected theories are finished;
4 months ago, by wenzelm
more accurate Word.capitalize: do not touch name;
4 months ago, by wenzelm
defer build until document nodes are ready;
4 months ago, by wenzelm
clarified signature: prefer semantic status;
4 months ago, by wenzelm
removed obsolete parameter (see 7c23db6b857b);
4 months ago, by wenzelm
clarified Document_Editor.Session: more explicit types, more robust operations;
4 months ago, by wenzelm
more operations;
4 months ago, by wenzelm
clarified operation (without change of signature!);
4 months ago, by wenzelm
pointless
4 months ago, by nipkow
Lots more new material thanks to Manuel Eberl
4 months ago, by paulson
merged
4 months ago, by paulson
Moved in a large number of highly useful library lemmas, mostly due to Manuel Eberl
4 months ago, by paulson
observe option "show_states" in headless server (see also 951abf9db857);
4 months ago, by wenzelm
text correction
4 months ago, by nipkow
enable clean_components by default: it saves a lot of local disk space, notably on virtual nodes;
4 months ago, by wenzelm
merged
4 months ago, by wenzelm
removed somewhat pointless support for Jenkins log files: it has stopped working long ago;
4 months ago, by wenzelm
more uniform components context for the managing "self_isabelle" and the managed "other_isabelle";
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
more operations;
4 months ago, by wenzelm
obsolete (see also d547173212d2);
4 months ago, by wenzelm
clarified names to emphasize suble differences in meaning;
4 months ago, by wenzelm
prefer high-level Other_Isabelle.bash over low-level SSH.execute;
4 months ago, by wenzelm
unused (see 378bb7a739c3);
4 months ago, by wenzelm
more options to manage resolved components;
4 months ago, by wenzelm
proper use of current ISABELLE_COMPONENT_REPOSITORY from the managing Isabelle system (amending 3e963d68d394);
4 months ago, by wenzelm
tuned comments;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified signature: more explicit types;
4 months ago, by wenzelm
more operations;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified signature: more robust field_scale;
4 months ago, by wenzelm
clarified signature: more explicit types;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
support units, e.g. java.lang.Long.MAX_VALUE is 8 EiB;
4 months ago, by wenzelm
more explicit types;
4 months ago, by wenzelm
prefer typed/strict operations;
4 months ago, by wenzelm
tuned message;
4 months ago, by wenzelm
prefer strict operation: java.io.File.length returns 0 for non-existent file;
4 months ago, by wenzelm
prefer typed bytes count, but retain toString of original Long for robustness of Java/Scala string composition;
4 months ago, by wenzelm
back to Scala 3.2.0 for now, since 3.2.1 causes odd crash of REPL concerning value classes (e.g. "isabelle.Time.now()");
4 months ago, by wenzelm
Restored antiquotation.
4 months ago, by haftmann
tuned whitespace
4 months ago, by haftmann
merged
4 months ago, by desharna
added lemma multpHO_plus_plus[simp]
4 months ago, by desharna
Shortened a messy proof
4 months ago, by paulson
Moved in some material from the AFP entry Winding_number_eval
4 months ago, by paulson
merged
4 months ago, by wenzelm
tuned messages: less verbosity;
4 months ago, by wenzelm
prefer Other_Isabelle.init instead of adhoc scripts;
4 months ago, by wenzelm
tuned message, following "isabelle components -a";
4 months ago, by wenzelm
clean components more accurately: purge other platforms or archives;
4 months ago, by wenzelm
more operations for SSH.System;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
manage other Isabelle distributions via SSH;
4 months ago, by wenzelm
more operations for SSH.System;
4 months ago, by wenzelm
recovered option -C from 092449efcb0e (still required for isabelle_cronjob.scala on Windows), but with slightly different meaning;
4 months ago, by wenzelm
clarified parameters (again);
4 months ago, by wenzelm
Some new material from the AFP
4 months ago, by paulson
clarified defaults: imitate "isabelle components -I" without further parameters;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
merged
4 months ago, by wenzelm
more robust locations (amending 7e11e96a922d) --- notably for cleanup() in build_release, after Admin/ been deleted;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified defaults (see also b310b93563f6);
4 months ago, by wenzelm
tuned comments;
4 months ago, by wenzelm
discontinued adhoc change of environment (from 897f1ac84aab), following ssh c2e8ba15a10a;
4 months ago, by wenzelm
more formal Other_Isabelle.settings, with derived expand_path / bash_path;
4 months ago, by wenzelm
clarified signature: minimal interface for getenv/expand_env, instead of bulky java.util.Map;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
discontinued adhoc change of environment (from c62b99e3ec07), which has been mostly superseded by expand_path / remote_path (from ef6f7e8a018c);
4 months ago, by wenzelm
more operations;
4 months ago, by wenzelm
removed unused user_home argument (see also 897f1ac84aab and 19b6091c2137);
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
more robust: self-contained Other_Isabelle.isabelle_home;
4 months ago, by wenzelm
more robust and uniform Other_Isabelle.scala_build;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
tuned message;
4 months ago, by wenzelm
more robust (see also 7f55a3e28c88): resolve components from current Isabelle context, using Isabelle/Scala instead of shell scripts;
4 months ago, by wenzelm
more strict;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
proper ssh.bash_path;
4 months ago, by wenzelm
merged
4 months ago, by desharna
added lemma irreflp_on_multpHO[simp]
4 months ago, by desharna
added lemmas totalp_on_multpDM, totalp_multpDM, totalp_on_multpHO, and totalp_multpHO
4 months ago, by desharna
Beautifying an old entry
4 months ago, by paulson
generalized theory name: euclidean division denotes one particular division definition on integers
4 months ago, by haftmann
merged
4 months ago, by wenzelm
support remote operations;
4 months ago, by wenzelm
more elementary command-line, following lib/Tools/components;
4 months ago, by wenzelm
clarified defaults;
4 months ago, by wenzelm
more accurate options (amending 7e19dc018db9);
4 months ago, by wenzelm
clarified defaults;
4 months ago, by wenzelm
support remote download_file;
4 months ago, by wenzelm
more modular shell script;
4 months ago, by wenzelm
more uniform options for "curl", following lib/Tools/components;
4 months ago, by wenzelm
tuned: drop redundant "expand";
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
added lemmas total_on_mult, total_mult, totalp_on_multp, and totalp_multp
4 months ago, by desharna
proper name for lemma totalp_on_total_on_eq
4 months ago, by desharna
update to jdk-17.0.6;
4 months ago, by wenzelm
proper cleanup;
4 months ago, by wenzelm
avoid odd suffix in published HTML library;
4 months ago, by wenzelm
tuned signature: avoid aliases;
4 months ago, by wenzelm
tuned message;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
clarified modules (again, in contrast to f8f065e20837);
4 months ago, by wenzelm
support IPC via database server;
4 months ago, by wenzelm
proper signature;
4 months ago, by wenzelm
support specific connection types, for additional operations;
4 months ago, by wenzelm
more correct and complete bibliography;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
proper position for semantic completion: avoid duplicate quotes;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
proper positions for Isabelle/ML, instead of Isabelle/Scala;
4 months ago, by wenzelm
dismantle special treatment of citations in Isabelle/Scala;
4 months ago, by wenzelm
more direct check of bibtex entries via Isabelle/Scala;
4 months ago, by wenzelm
support Session argument for Scala.Fun;
4 months ago, by wenzelm
obsolete (see also 01c9b3033036);
4 months ago, by wenzelm
proper citations for unselected theories, notably for the default selection of the GUI panel;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
merged
4 months ago, by wenzelm
clarified "selected" status;
4 months ago, by wenzelm
uniform keywords for embedded syntax;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
more complete index;
4 months ago, by wenzelm
tuned comments;
4 months ago, by wenzelm
parse citations from raw source, without formal context;
4 months ago, by wenzelm
tuned signature: fewer warnings in IntelliJ IDEA;
4 months ago, by wenzelm
tuned messages;
4 months ago, by wenzelm
tuned GUI;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
more efficient, thanks to persistent lazy data in Document.Node;
4 months ago, by wenzelm
proper line positions for PIDE document;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
HOL/Library/BigO is obsolete
4 months ago, by paulson
merged
4 months ago, by paulson
tidy up of this messy and obsolete theory
4 months ago, by paulson
clarified file positions: retain original source path;
4 months ago, by wenzelm
backed out changeset 7f7d5c93e36b: no longer required thanks to 9096703ed99e;
4 months ago, by wenzelm
clarified formal check of bibtex entries (again), see also 86a099f896fc and 467f45e79ff9;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
tuned GUI;
4 months ago, by wenzelm
permissive treatment of citations before the theory header: avoid too many changes in AFP;
4 months ago, by wenzelm
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
4 months ago, by wenzelm
clarified documentation: avoid odd speculations about PIDE;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified modules;
4 months ago, by wenzelm
merged
4 months ago, by wenzelm
more complete Bibtex database;
4 months ago, by wenzelm
proper theory context for formal citations;
4 months ago, by wenzelm
isabelle update -u cite;
4 months ago, by wenzelm
clarified treatment of cite macro name;
4 months ago, by wenzelm
explicit legacy_feature;
4 months ago, by wenzelm
more robust: rely on PIDE markup instead of regex guess;
4 months ago, by wenzelm
more index entries;
4 months ago, by wenzelm
updated documentation;
4 months ago, by wenzelm
clarified names;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified options and defaults: avoid accidental changed of base logic due to augment_options(update_options);
4 months ago, by wenzelm
update documentation: prefer control-symbol-cartouche form of "cite" antiquotations;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
proper language context;
4 months ago, by wenzelm
proper normal form of adjacent XML.Text, notably for Bibtex.update_cite;
4 months ago, by wenzelm
tuned whitespace;
4 months ago, by wenzelm
more robust;
4 months ago, by wenzelm
basic support for update_cite_commands;
4 months ago, by wenzelm
more operations: use proper constants;
4 months ago, by wenzelm
proper session_options (amending da13da82f6f9);
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified types;
4 months ago, by wenzelm
more explicit language context;
4 months ago, by wenzelm
clarified signature: more explicit types;
4 months ago, by wenzelm
support embedded syntax, for use with control symbols;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified default: final value is provided in Isabelle/Scala Latex.Cite.unapply;
4 months ago, by wenzelm
more "cite" antiquotations;
4 months ago, by wenzelm
clarified signature: more generic operations;
4 months ago, by wenzelm
clarified check: this could be \nocite;
4 months ago, by wenzelm
avoid confusion of markup element vs. property names;
4 months ago, by wenzelm
clarified Latex markup: optional cite "location" consists of nested document text;
4 months ago, by wenzelm
more explicit latex markup;
4 months ago, by wenzelm
follow recent changes of Sledgehammer defaults, as 0a46b3dbd5ad exposes a hint in the source text;
4 months ago, by wenzelm
One messy, messy proof
4 months ago, by paulson
Missing theorem restored
4 months ago, by paulson
Tidying up BNF
4 months ago, by paulson
More cleaning up proofs, plus a TeX fix
4 months ago, by paulson
Fixed a broken proof
4 months ago, by paulson
Substantial simplification of HOL-Cardinals
4 months ago, by paulson
merged
4 months ago, by paulson
Trying to clean up HOL/Cardinals
4 months ago, by paulson
added session to mirabelle output directory structure
4 months ago, by desharna
More tidying of topology proofs
4 months ago, by paulson
Partial round of clearing up applys, etc
4 months ago, by paulson
merged
4 months ago, by paulson
merged
4 months ago, by paulson
Substantial de-applying and streamlining
4 months ago, by paulson
tuned sledgehammer default provers to only include local ones
4 months ago, by desharna
enforce rebuild of Isabelle/ML to update build databases;
4 months ago, by wenzelm
prefer relative src_path (if possible) -- in contrast to 9ce0aa145d21:
4 months ago, by wenzelm
proper treatment of unicode_symbols;
4 months ago, by wenzelm
tuned signature: avoid alias that is unclear wrt. lazy state and Symbol.encode/decode status;
4 months ago, by wenzelm
removed unused operation: unclear wrt. Symbol.encode/decode status;
4 months ago, by wenzelm
tuned signature: more uniform operations;
4 months ago, by wenzelm
tuned comments;
4 months ago, by wenzelm
unused;
4 months ago, by wenzelm
more uniform operations;
4 months ago, by wenzelm
restrict to proper_session_theories;
4 months ago, by wenzelm
proper build parameters (amending d858e6f15da3);
4 months ago, by wenzelm
treat update_options as part of Sessions.Info meta_digest, for proper re-build of updated sessions;
4 months ago, by wenzelm
more command-line options;
4 months ago, by wenzelm
tuned options --- avoid confusion with "isabelle build -b";
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
isabelle update -u path_cartouches;
4 months ago, by wenzelm
merged
4 months ago, by wenzelm
updated documentation;
4 months ago, by wenzelm
more options;
4 months ago, by wenzelm
tuned message;
4 months ago, by wenzelm
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
4 months ago, by wenzelm
more robust;
4 months ago, by wenzelm
more operations;
4 months ago, by wenzelm
proper Node.init_blobs, not just edits (amending ca872f20cf5b);
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
clarified session sources: theory and blobs are read from database, instead of physical file-system;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified signature: more operations;
4 months ago, by wenzelm
clarified signature: more operations;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
more direct access to session_sources, without somewhat fragile file-system operations;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
tuned signature;
4 months ago, by wenzelm
tuned signature: avoid confusion with Document.Node.Blob and Command.Blob;
4 months ago, by wenzelm
clarified signature: old node is ignored;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified signature;
4 months ago, by wenzelm
final tidying of theorems
4 months ago, by paulson
merged
4 months ago, by paulson
merged
4 months ago, by paulson
continued proof simplification
4 months ago, by paulson
merged
4 months ago, by paulson
Further simplifications
4 months ago, by paulson
More tidying of proofs
4 months ago, by paulson
tuned;
4 months ago, by wenzelm
merged
4 months ago, by wenzelm
discontinued fragile operation;
4 months ago, by wenzelm
more robust operations: avoid somewhat fragile Document.Node.Name.master_dir_path;
4 months ago, by wenzelm
tuned whitespace;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
avoid somewhat fragile Document.Node.Name.master_dir_path;
4 months ago, by wenzelm
clarified signature: avoid somewhat fragile Document.Node.Name.master_dir_path;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified modules;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
tuned;
4 months ago, by wenzelm
clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
4 months ago, by wenzelm
tuned signature: avoid too many aliases (see also 72daee8a39ca);
4 months ago, by wenzelm
clarified modules;
4 months ago, by wenzelm
merged
4 months ago, by desharna
strengthened and renamed lemmas asym_on_iff_irrefl_on_if_trans and asymp_on_iff_irreflp_on_if_transp
5 months ago, by desharna
Fixed a couple of simple_path occurrences
4 months ago, by paulson
merged
4 months ago, by paulson
Tidying up of paths, introducing "loop_free" as a separate predicate in the definition of "simple_path"
4 months ago, by paulson
clarified signature: more explicit types;
4 months ago, by wenzelm
more robust: prefer internal theory names;
4 months ago, by wenzelm
clarified session_sources (again, see also 9d0e6ea7aa68);
5 months ago, by wenzelm
clarified signature: more explicit types;
5 months ago, by wenzelm
tuned output;
5 months ago, by wenzelm
clarified signature: more general operations;
5 months ago, by wenzelm
clarified signature: more explicit types;
5 months ago, by wenzelm
clarified signature: more explicit types (see also 90c552d28d36);
5 months ago, by wenzelm
do write_session_sources early, to have information available in build job;
5 months ago, by wenzelm
tuned signature, following Url.append_path;
5 months ago, by wenzelm
do not bundle Isabelle/Naproche, while it keeps changing;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified signature: uniform master_dir instead of separate field;
5 months ago, by wenzelm
more standard master_dir;
5 months ago, by wenzelm
tuned signature, following Url.append_path;
5 months ago, by wenzelm
merged
5 months ago, by wenzelm
more robust, for the sake of very rare duplicate files: src/Doc/Prog_Prove/MyList.thy and $AFP/Case_Labeling/util.ML;
5 months ago, by wenzelm
store session sources within build database: timing e.g. 150ms for HOL and < 50ms for common sessions;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tunes signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
more systematic Sessions.illegal_theory, based on File_Format.theory_excluded;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
unused;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
tuned: no need to map master_dir, which does not participate in comparison;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
tuned comments;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
removed an unfortunate sledgehammer command
5 months ago, by paulson
A couple of patches
5 months ago, by paulson
Big simplifications of old proofs
5 months ago, by paulson
repaired a proof
5 months ago, by paulson
Continued proof simplifications
5 months ago, by paulson
merged
5 months ago, by paulson
A further round of proof consolidation
5 months ago, by paulson
tuned signature: avoid too many aliases;
5 months ago, by wenzelm
proper thread context (amending 01a7265db76b) -- at the danger of blocking the GUI;
5 months ago, by wenzelm
more robust: avoid detour via somewhat fragile Node.Name.path;
5 months ago, by wenzelm
clarified generic path operations;
5 months ago, by wenzelm
more flexible: implicit support for Windows;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
clarified output;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
merged
5 months ago, by paulson
More tidying
5 months ago, by paulson
Further cleaning up of messy proofs
5 months ago, by paulson
merged
5 months ago, by paulson
reorganisation and simplification of theorems about transcendental functions
5 months ago, by paulson
tuned signature;
5 months ago, by wenzelm
support asynchronous presentation commands, but not for "no_update" / "Keep", which is usually forked via "Toplevel.diag";
5 months ago, by wenzelm
tuned whitespace;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
discontinued somewhat pointless exception FAILURE with its "alt_state", which was originally due to quasi-mutable states (see 169e5b07ec06);
5 months ago, by wenzelm
tuned --- more robust ML patterns;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
merged
5 months ago, by wenzelm
tuned signature, for the sake of AFP/Isabelle_C;
5 months ago, by wenzelm
more uniform report of Markup.language_path;
5 months ago, by wenzelm
omit pointless guard: ultimately observed by Isabelle_Process.report_message;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned output;
5 months ago, by wenzelm
merged
5 months ago, by paulson
Tidied some messy proofs
5 months ago, by paulson
merged
5 months ago, by wenzelm
clarified modules: avoid duplication;
5 months ago, by wenzelm
tuned output;
5 months ago, by wenzelm
support for generic File_Format.parse_data, with persistent result in document model;
5 months ago, by wenzelm
omit warning: somewhat pointless and out-of-context;
5 months ago, by wenzelm
clarified signature: avoid case class with mutable state;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified signature: more explicit types;
5 months ago, by wenzelm
merged
5 months ago, by paulson
tidied some messy old proofs
5 months ago, by paulson
tuned signature;
5 months ago, by wenzelm
merged
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
more robust;
5 months ago, by wenzelm
clarified signature: more position information via node_name;
5 months ago, by wenzelm
tuned signature: avoid name confusion;
5 months ago, by wenzelm
more bibtex errors;
5 months ago, by wenzelm
clarified signature: internalize errors (but: the parser rarely fails);
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
clarified signature: more explicit types;
5 months ago, by wenzelm
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
5 months ago, by wenzelm
merged
5 months ago, by desharna
removed old lemma names
5 months ago, by desharna
merged
5 months ago, by paulson
merged
5 months ago, by paulson
A few new Sup/Inf lemmas
5 months ago, by paulson
clarified messages;
5 months ago, by wenzelm
tuned signature: follow terminology of VSCode_Resources;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
5 months ago, by wenzelm
update URL;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified signature: more explicit types;
5 months ago, by wenzelm
merged
5 months ago, by desharna
merged
5 months ago, by desharna
used transp_on in assumptions of lemmas Multiset.bex_(least|greatest)_element
5 months ago, by desharna
added lemma trans_on_lex_prod[simp]
5 months ago, by desharna
strengthened and renamed lemma trans_converse and added lemma transp_on_conversep
5 months ago, by desharna
strengthened and renamed trans_reflclI
5 months ago, by desharna
strengthened and renamed transp_reflclp
5 months ago, by desharna
strengthened and renamed lemmas preorder.transp_(ge|gr|le|less)
5 months ago, by desharna
added lemmas trans_on_subset and transp_on_subset
5 months ago, by desharna
added lemmas trans_onD and transp_onD
5 months ago, by desharna
added lemmas trans_onI and transp_onI
5 months ago, by desharna
added lemma transp_on_trans_on_eq[pred_set_conv]
5 months ago, by desharna
fixed code-generation failure
5 months ago, by desharna
added predicates trans_on and transp_on and redefined trans and transp to be abbreviations
5 months ago, by desharna
only show sessions with document setup;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
proper node name instead of not base tex_name (amending 2fd0c33fe440);
5 months ago, by wenzelm
proper migrate_name between different kinds of Resources, notably for Windows;
5 months ago, by wenzelm
merged
5 months ago, by desharna
added lemmas irrefl_on_if_asym_on[simp] and irreflp_on_if_asymp_on[simp]
5 months ago, by desharna
proper PIDE session background for interactive document context;
5 months ago, by wenzelm
NEWS;
5 months ago, by wenzelm
more accurate error messages;
5 months ago, by wenzelm
merged
5 months ago, by wenzelm
actually build document;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
tuned comments;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified GUI;
5 months ago, by wenzelm
more thorough GUI updates, notably for multiple Document dockables;
5 months ago, by wenzelm
Additional new material about infinite products, etc.
5 months ago, by paulson
merged
5 months ago, by paulson
First round of moving material from the number theory development
5 months ago, by paulson
merged
5 months ago, by wenzelm
more GUI operations;
5 months ago, by wenzelm
proper handling of state updates;
5 months ago, by wenzelm
clarified process management;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
clarified state document nodes for Theories_Status / Document_Dockable;
5 months ago, by wenzelm
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
5 months ago, by wenzelm
tuned whitespace;
5 months ago, by wenzelm
clarified module initialization;
5 months ago, by wenzelm
tuned signature, following Document_Dockable;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
clarified GUI;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
proper thread context;
5 months ago, by wenzelm
more informative errors, including optional Exn.trace;
5 months ago, by wenzelm
clarified state change: presumably more robust;
5 months ago, by wenzelm
proper state change, e.g. on open/close of "Document" panel;
5 months ago, by wenzelm
clarified module initialization;
5 months ago, by wenzelm
clarified state: node_required is guarded by PIDE.editor.document_active (e.g. open panel);
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
added lifting_forget as suggested by Peter Lammich
5 months ago, by blanchet
merged
5 months ago, by desharna
added lemma refl_lex_prod[simp]
5 months ago, by desharna
added lemmas reflI and reflD
5 months ago, by desharna
added lemmas asym_on_lex_prod[simp] and asym_lex_prod[simp]
5 months ago, by desharna
added lemmas sym_on_lex_prod[simp] and sym_lex_prod[simp]
5 months ago, by desharna
added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp]
5 months ago, by desharna
strengthened and renamed lemmas asym_if_irrefl_and_trans and asymp_if_irreflp_and_transp
5 months ago, by desharna
strengthened and renamed lemma antisym_converse and added lemma antisymp_on_conversep
5 months ago, by desharna
added lemmas asym_on_converse[simp] and asymp_on_conversep[simp]
5 months ago, by desharna
strengthened and renamed lemma sym_converse and added lemma symp_on_conversep
5 months ago, by desharna
strengthened and renamed lemmas antisymp_less and antisymp_greater
5 months ago, by desharna
strengthened lemmas antisym_on_if_asym_on and antisymp_on_if_asymp_on
5 months ago, by desharna
tuned naming
5 months ago, by desharna
added lemma asymp_on_asym_on_eq[pred_set_conv]
5 months ago, by desharna
strengthened and renamed asymp_less and asymp_greater
5 months ago, by desharna
added lemmas asym_on_subset and asymp_on_subset
5 months ago, by desharna
added lemmas asym_onI, asymp_onI, asym_onD, and asymp_onD
5 months ago, by desharna
added predicates asym_on and asymp_on and redefined asym and asymp to be abbreviations
5 months ago, by desharna
clarified state and process;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
merged
5 months ago, by desharna
strengthened and renamed symp_symclp
5 months ago, by desharna
merged
5 months ago, by nipkow
Tuned text
5 months ago, by nipkow
clarified signature: avoid confusion due to redundant standard_path, which is already used here (but not elsewhere);
5 months ago, by wenzelm
clarified signature: avoid case class with redefined equality;
5 months ago, by wenzelm
discontinued somewhat pointless dependency: avoid illusion of extra accuracy (see also 09fb749d1a1e and 0f750a6dc754);
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
unused;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned whitespace;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
tuned output;
5 months ago, by wenzelm
prefer SML here
5 months ago, by haftmann
Typo.
5 months ago, by haftmann
merged
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified names;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
tuned signature (see also 8342cba8eae8);
5 months ago, by wenzelm
tuned names: avoid overlap with instances of class Resources;
5 months ago, by wenzelm
merged
5 months ago, by nipkow
file with partial function docu
5 months ago, by nipkow
Added section about code generation for partial functions
5 months ago, by nipkow
added lemmas sym_on_subset and symp_on_subset
5 months ago, by desharna
added lemmas sym_onD and symp_onD
5 months ago, by desharna
added lemmas sym_onI and symp_onI
5 months ago, by desharna
added lemma symp_on_sym_on_eq[pred_set_conv]
5 months ago, by desharna
added predicates sym_on and symp_on and redefined sym and symp to be abbreviations
5 months ago, by desharna
added lemmas IMGU_subst_domain_subset and IMGU_range_vars_subset
5 months ago, by desharna
added lemmas antisym_on_subset and antisymp_on_subset
5 months ago, by desharna
strengthened antisymp_le and antisymp_ge
5 months ago, by desharna
added lemmas antisym_onD and antisymp_onD
5 months ago, by desharna
added lemmas antisym_onI and antisymp_onI
5 months ago, by desharna
added lemma antisymp_reflcp
5 months ago, by desharna
added antisymp_on_antisym_on_eq[pred_set_conv]
5 months ago, by desharna
added predicates antisym_on and antisymp_on and redefined antisym and antisymp to be abbreviations
5 months ago, by desharna
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified order: accumulate strictly from left to right;
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
clarified signature: more types and operations;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
proper file extension for Isabelle_System.extract;
5 months ago, by wenzelm
tuned implementation;
5 months ago, by wenzelm
more uniform use of make_directory;
5 months ago, by wenzelm
tuned message;
5 months ago, by wenzelm
tuned: less redundant implementation;
5 months ago, by wenzelm
clarified signature: copy directory content more directly;
5 months ago, by wenzelm
more robust;
5 months ago, by wenzelm
tuned whitespace;
5 months ago, by wenzelm
clarified signature: more general operations;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
merged
5 months ago, by desharna
Strengthened multiset lemmas w.r.t. irrefl and irreflp
5 months ago, by desharna
clarified signature: proper scopes and types;
5 months ago, by wenzelm
maintain global state of document editor views, notably for is_active operation;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
tuned whitespace;
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
clarified signature: more robust;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
more specific GUI for document nodes;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
merged
5 months ago, by wenzelm
clarified signature: just one level of arguments to avoid type-inference problems;
5 months ago, by wenzelm
tuned signature: more operations;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
stated goals of some lemmas explicitely to prevent silent changes
5 months ago, by desharna
rewrite proofs using to_pred attribute on existing lemmas
5 months ago, by desharna
clarified signature: less redundancy;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
potentially more robust delay_load action: avoid loosing events due to guards;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
more uniform tooltip for plugin options dialog;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
more uniform session selectors, with persistent options;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
NEWS
5 months ago, by desharna
merged
5 months ago, by desharna
added lemmas asym_if_irrefl_and_trans and asymp_if_irreflp_and_transp
6 months ago, by desharna
added lemma totalp_on_converse[simp]
6 months ago, by desharna
added lemmas irrefl_on_converse[simp] and irreflp_on_converse[simp]
6 months ago, by desharna
added type annotations and tuned formatting
6 months ago, by desharna
strengthened and renamed irreflp_greater[simp] and irreflp_less[simp]
6 months ago, by desharna
merged
5 months ago, by wenzelm
tuned GUI behaviour;
5 months ago, by wenzelm
more GUI elements;
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
clarified process: implicit load() when finished;
5 months ago, by wenzelm
more robust, notably initial update();
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned messages: implement "verbose = false", but there is no theory output anyway;
5 months ago, by wenzelm
merged
5 months ago, by desharna
added lemmas irrefl_on_subset and irreflp_on_subset
6 months ago, by desharna
introduced predicates irrefl_on and irreflp_on, and redefined irrefl and irreflp as abbreviations
6 months ago, by desharna
tuned messages;
5 months ago, by wenzelm
tuned message;
5 months ago, by wenzelm
tuned messages and options;
5 months ago, by wenzelm
merged
5 months ago, by desharna
removed prod_set_conv attribute from top_empty_eq and top_empty_eq2
6 months ago, by desharna
discontinued "unzip" executable (see also eb96243a25c5 and 662de910a96b);
5 months ago, by wenzelm
more direct access to jEdit jar resources, without unzip;
5 months ago, by wenzelm
clarified check: allow to remove bad directories;
6 months ago, by wenzelm
clarified check;
6 months ago, by wenzelm
tuned message;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
proper unzip with strip option, within the JVM;
6 months ago, by wenzelm
updated to sqlite-jdbc-3.39.4.1;
6 months ago, by wenzelm
more standard component build process;
6 months ago, by wenzelm
clarified signature: prefer Scala functions instead of shell scripts;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
more direct target directory;
6 months ago, by wenzelm
clarified signature: prefer Scala functions instead of shell scripts;
6 months ago, by wenzelm
A new Isabelle/CTT example, and eliminated some old-style quotation marks
6 months ago, by paulson
clarified exception: avoid odd compiler warning;
6 months ago, by wenzelm
update to scala-3.2.1;
6 months ago, by wenzelm
recovered check from 69139cc01ba1: Windows does not support PosixFilePermission;
6 months ago, by wenzelm
update to jdk-17.0.5 (Oct-2022);
6 months ago, by wenzelm
more standard component build process;
6 months ago, by wenzelm
proper treatment of tar.gz double-extension;
6 months ago, by wenzelm
proper download, instead of assuming local directory;
6 months ago, by wenzelm
more standard component build process;
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
discontinue unused JCEF: superseded by Electron with its bundled Chromium;
6 months ago, by wenzelm
prefer deterministic result;
6 months ago, by wenzelm
clarified command-line arguments: follow more recent isabelle build_XYZ;
6 months ago, by wenzelm
compile
6 months ago, by blanchet
correctly show '(> 2 s, timed out)' or similar in Sledgehammer's output
6 months ago, by blanchet
merged
6 months ago, by desharna
strengthened and renamed lemma reflp_on_equality
6 months ago, by desharna
renamed lemmas linorder.totalp_on_(ge|greater|le|less) and preorder.reflp_(ge|le)
6 months ago, by desharna
Added an example for Isabelle/CTT
6 months ago, by paulson
clarified signature;
6 months ago, by wenzelm
clarified signature: more explicit types;
6 months ago, by wenzelm
tuned output;
6 months ago, by wenzelm
prefer sorted result;
6 months ago, by wenzelm
separate style for re-use;
6 months ago, by wenzelm
ML support for the Prism.js syntax highlighter -- via Isabelle/Scala;
6 months ago, by wenzelm
retain data structures more accurately;
6 months ago, by wenzelm
proper join without delimiter;
6 months ago, by wenzelm
more accurate token types;
6 months ago, by wenzelm
clarified JS namespace;
6 months ago, by wenzelm
proper support for Windows;
6 months ago, by wenzelm
support for the Prism.js syntax highlighter -- via external Node.js process;
6 months ago, by wenzelm
support for JavaScript syntax and Node.js platform;
6 months ago, by wenzelm
merged
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
clarified signature: ensure that entries are well-formed --- no consecutive separators, no separators at start/end;
6 months ago, by wenzelm
clarified signature: only support nameless separator;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
use timeout with MiniSat
6 months ago, by blanchet
merged
6 months ago, by desharna
added lemma reflp_on_conversp[simp]
6 months ago, by desharna
added lemma transp_reflclp[simp]
6 months ago, by desharna
added lemma reflclp_ident_if_reflp[simp]
6 months ago, by desharna
added lemma reflp_on_reflclp[simp]
6 months ago, by desharna
strengthened lemma reflp_rtranclp and renamed to reflp_on_rtranclp
6 months ago, by desharna
more robust selection: avoid duplicates via "batch" number;
6 months ago, by wenzelm
tuned GUI;
6 months ago, by wenzelm
clarified GUI.Selector, with support for separator as pseudo-entry;
6 months ago, by wenzelm
clarified GUI state;
6 months ago, by wenzelm
clarified file names;
6 months ago, by wenzelm
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
6 months ago, by wenzelm
clarified signature: more public operations;
6 months ago, by wenzelm
tuned signature, following hints by IntelliJ IDEA;
6 months ago, by wenzelm
merged
6 months ago, by nipkow
retain derived lemma for better findability
6 months ago, by nipkow
generalized sorted_sort_id to sort_key_id_if_sorted
6 months ago, by nipkow
suppress document_required GUI element for now: still unused;
6 months ago, by wenzelm
clarified layout;
6 months ago, by wenzelm
clarified node_required status: distinguish theory_required vs. document_required;
6 months ago, by wenzelm
proper user tool;
6 months ago, by wenzelm
tuned comments;
6 months ago, by wenzelm
support for EPTCS style with demo document;
6 months ago, by wenzelm
tuned message;
6 months ago, by wenzelm
clarified delay -- more reactive;
6 months ago, by wenzelm
provide Session.init_time as reference point for diagnostic messages;
6 months ago, by wenzelm
afford more reactive consolidation;
6 months ago, by wenzelm
minor performance tuning;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
afford unconditional presentation, notably export_theory and present_thy, notably for HTML + PDF presentation within PIDE;
6 months ago, by wenzelm
proper executable files for Windows;
6 months ago, by wenzelm
further attempts to confine dotnet to $ISABELLE_HOME_USER;
6 months ago, by wenzelm
tuned output;
6 months ago, by wenzelm
more command-line options;
6 months ago, by wenzelm
clarified component settings: always update existing version;
6 months ago, by wenzelm
more TODO for release;
6 months ago, by wenzelm
disable telemetry;
6 months ago, by wenzelm
clarified error;
6 months ago, by wenzelm
tuned message, example is in NEWS;
6 months ago, by wenzelm
proper default_platform;
6 months ago, by wenzelm
tuned NEWS;
6 months ago, by wenzelm
tuned message;
6 months ago, by wenzelm
support for Dotnet / Fsharp platform, via dynamically installed Isabelle component;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
tuned comments;
6 months ago, by wenzelm
clarified description, to fit better to e.g. "isabelle build_doc -a -V system jedit";
6 months ago, by wenzelm
clarified options: support lualatex as well, but prefer old pdflatex for demos;
6 months ago, by wenzelm
more command-line options;
6 months ago, by wenzelm
proper URL;
6 months ago, by wenzelm
document_build engine for "lipics", with options and document_files;
6 months ago, by wenzelm
clarified signature: allow to change options in instances of Document_Build.Engine;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
clarified options: LLNCS works with LuaLaTeX and Isabelle sections, although Springer might not like it;
6 months ago, by wenzelm
Better use the finite simproc selectively only
6 months ago, by nipkow
tuned document;
6 months ago, by wenzelm
tuned document;
6 months ago, by wenzelm
clarified LaTeX style;
6 months ago, by wenzelm
support for Springer LLNCS with demo document;
6 months ago, by wenzelm
prefer explicit utf8 for old pdflatex;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
proper chapter (amending 809cd1195795);
6 months ago, by wenzelm
merged
6 months ago, by wenzelm
tuned (again);
6 months ago, by wenzelm
prefer strict operation (see also f29056da5903);
6 months ago, by wenzelm
more antiquotations;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
prefer strict operation;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
misc tuning;
6 months ago, by wenzelm
clarified options;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
merged
6 months ago, by nipkow
added finite simproc
7 months ago, by nipkow
merged
6 months ago, by wenzelm
clarified directory layout: templates for user sessions;
6 months ago, by wenzelm
tuned proofs;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
proper pattern (amending 40a365360680);
7 months ago, by wenzelm
more timing;
7 months ago, by wenzelm
tuned;
7 months ago, by wenzelm
tuned comments;
7 months ago, by wenzelm
tuned;
7 months ago, by wenzelm
prefer abstract command kind (in contrast to 367f4512e65c);
7 months ago, by wenzelm
tuned;
7 months ago, by wenzelm
tuned: avoid warning in IntelliJ IDEA;
7 months ago, by wenzelm
more accurate outer syntax keywords (see also 94b2690ad494): base session could be anything, e.g. ZF vs. HOL;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
clarified signature: do not require finished theory;
7 months ago, by wenzelm
clarified modules;
7 months ago, by wenzelm
merged
7 months ago, by desharna
added lemmas multp_mono_strong and mult_mono_strong
7 months ago, by desharna
merged
7 months ago, by wenzelm
support for FoilTeX with demo document;
7 months ago, by wenzelm
tuned comments;
7 months ago, by wenzelm
tuned whitespace for "isabelle doc" display;
7 months ago, by wenzelm
support for Easychair style with demo document;
7 months ago, by wenzelm
support for Dagstuhl LIPIcs style with demo document;
7 months ago, by wenzelm
clarified signature;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
tuned;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
clarified modules;
7 months ago, by wenzelm
tuned;
7 months ago, by wenzelm
tuned signature, following hints by IntelliJ IDEA;
7 months ago, by wenzelm
restructured
7 months ago, by haftmann
modulus for polynomials is invariant wrt. units
7 months ago, by haftmann
proper Java syntax (amending ea79c21bcc47);
7 months ago, by wenzelm
reactivate emerging tool after release (see 322f2e2799a7);
7 months ago, by wenzelm
separate out definition of bound to avoid spurious sort hypotheses (by Jan van Brügge)
7 months ago, by traytel
merged
7 months ago, by paulson
Beautification of some declarations
7 months ago, by paulson
merged
7 months ago, by wenzelm
more robust etc/preferences: default value remains;
7 months ago, by wenzelm
formal bundling for Admin/build_release: avoid confusion about presence or absence in manual invocations;
7 months ago, by wenzelm
Beautifying CTT a tiny bit
7 months ago, by paulson
A couple of new theorems. Also additional coercions to the complex numbers
7 months ago, by paulson
more macOS platforms, without reference hardware;
7 months ago, by wenzelm
official release;
7 months ago, by wenzelm
merged
7 months ago, by wenzelm
Added tag Isabelle2022 for changeset 1ac2416e8432
7 months ago, by wenzelm
tuned signature (again, amending f32ac01aef5e), e.g. relevant for Isabelle/DOF;
Isabelle2022
7 months ago, by wenzelm
tuned signature, e.g. for Isabelle/DOF;
7 months ago, by wenzelm
updated to naproche-20221024: minor changes to documentation;
7 months ago, by wenzelm
Replaced some ugly legacy proofs
7 months ago, by paulson
more thorough cleanup;
7 months ago, by wenzelm
tuned;
7 months ago, by wenzelm
tuned: more robust Scala syntax;
7 months ago, by wenzelm
merged
7 months ago, by wenzelm
no compression for database server: let PostgreSQL/TOAST do the job;
7 months ago, by wenzelm
prefer Zstd compression, notably for database exports;
7 months ago, by wenzelm
tuned: avoid redundant copy of potentially large array;
7 months ago, by wenzelm
merged
7 months ago, by desharna
tuned proof
7 months ago, by desharna
clarified signature;
7 months ago, by wenzelm
tuned signature, following isabelle.setup.Environment;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
clarified signature;
7 months ago, by wenzelm
prefer new instance, following "make" signature terminology;
7 months ago, by wenzelm
generic support for XZ and Zstd compression in Isabelle/Scala;
7 months ago, by wenzelm
clarified signature: default cache is actually dummy and not changed dynamically;
7 months ago, by wenzelm
clarified Zstd.init(): avoid accidential com.github.luben.zstd.util.Native.load() operation;
7 months ago, by wenzelm
support for Zstd data compression;
7 months ago, by wenzelm
enforce fresh build;
7 months ago, by wenzelm
merged
7 months ago, by wenzelm
more robust read_file: prefer implicit replacement of bad input instead of failure via MalformedInputException;
7 months ago, by wenzelm
more informative errors, with optional exception trace as in Command_Line.tool;
7 months ago, by wenzelm
more robust reset of CLASSPATH: unset variable means "." in certain situations, e.g. scalac;
7 months ago, by wenzelm
proper chapter for each ROOT file (amending b07f2ff55144);
7 months ago, by wenzelm
tidying of ugly legacy proofs
7 months ago, by paulson
Tidying of old and ugly proofs
7 months ago, by paulson
deleted unused material
7 months ago, by paulson
A bit of tidying
7 months ago, by paulson
merged
7 months ago, by paulson
Slight tidying of legacy proofs
7 months ago, by paulson
merged
7 months ago, by wenzelm
update naproche component;
7 months ago, by wenzelm
Added tag Isabelle2022-RC4 for changeset 8b4108f41c77
7 months ago, by wenzelm
rebuild with proper Isabelle version;
7 months ago, by wenzelm
removed junk;
7 months ago, by wenzelm
more robust, e.g. for "isabelle dump";
7 months ago, by wenzelm
more robust, e.g. for "isabelle dump";
7 months ago, by wenzelm
more robust, e.g. for "isabelle dump";
7 months ago, by wenzelm
allow spaces in SCALA_HOME directory name;
7 months ago, by wenzelm
avoid spurious error messages, e.g. when scala is missing;
7 months ago, by wenzelm
more NEWS;
7 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
7 months ago, by wenzelm
avoid result based on outdated state, e.g. relevant for use_theories with changed files;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
tuned signature, following hints by IntelliJ IDEA;
7 months ago, by wenzelm
more robust treatment of state and events;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
proper result state (amending 954640e846d6);
7 months ago, by wenzelm
tuned;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
tuned;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
tuned: clarified old_theory (in contrast to 4d5342898b1);
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
more robust: active consumer for check_state/check_progress;
7 months ago, by wenzelm
proper update of non-committed theories (see also 2bf1d0e57695, 2a1583baaaa0);
7 months ago, by wenzelm
tuned;
7 months ago, by wenzelm
tuned;
7 months ago, by wenzelm
proper Symbol.encode (following fd1efd6dd385), e.g. relevant for 'ML_file' with symbols like \<^here>;
7 months ago, by wenzelm
merged
7 months ago, by desharna
added lemma fmember_iff_member_fset
7 months ago, by desharna
tiny renaming
7 months ago, by paulson
merged
7 months ago, by paulson
Added the multiset termination proof
7 months ago, by paulson
generate some metainformation not only for SPASS but also for Zipperposition, for experimentation
7 months ago, by blanchet
added lemma wfP_subset_mset[simp]
7 months ago, by desharna
Tidying of some very old proofs
7 months ago, by paulson
merged
7 months ago, by paulson
tidying of some old proofs
7 months ago, by paulson
merged
7 months ago, by nipkow
new contributor
7 months ago, by nipkow
more List lemmas (partly by Jeremy Sylvestre)
7 months ago, by nipkow
merged
7 months ago, by paulson
merged
7 months ago, by paulson
Trying to clean up some messy proofs
7 months ago, by paulson
Mostly, removing the unfold method
7 months ago, by paulson
Mostly trivial simplifications
7 months ago, by paulson
Removal of the "unfold" method in favour of "unfolding"
7 months ago, by paulson
Elimination of the archaic ASCII syntax
7 months ago, by paulson
strengthened lemmas preorder.reflp_ge[simp] and preorder.reflp_le[simp]
7 months ago, by desharna
added lemmas linorder.totalp_ge[simp], linorder.totalp_greater[simp], linorder.totalp_le[simp], and linorder.totalp_less[simp]
7 months ago, by desharna
NEWS
7 months ago, by desharna
merged
7 months ago, by desharna
fixed NEWS following cee0b9fccf6f
7 months ago, by desharna
renamed lemma inj_on_strict_subset to image_strict_mono for symmetry with image_mono and to distinguish from inj_on_subset
7 months ago, by desharna
merged
7 months ago, by wenzelm
proper Deps.is_empty (amending 77327455b00d), e.g. relevant for warning "Nothing to build";
7 months ago, by wenzelm
tuned whitespace;
7 months ago, by wenzelm
less ambitious Bytes.chunk_size, which is presumably more stable with memory management under heavy load;
7 months ago, by wenzelm
tuned comment;
7 months ago, by wenzelm
support for system option ML_system_apple: emulated x86_64 Poly/ML is sometimes more stable than native ARM64;
7 months ago, by wenzelm
updated to repository version polyml-test-bafe319bc3a6, which is presumably more stable (especially for ARM64);
7 months ago, by wenzelm
more robust: prefer Windows $USERNAME;
7 months ago, by wenzelm
proper home directory for ssh configuration (e.g. ~/.ssh/config);
7 months ago, by wenzelm
more NEWS;
7 months ago, by wenzelm
clarified signature: more arguments;
7 months ago, by wenzelm
added lemma fimage_strict_mono
7 months ago, by desharna
added lemma wfP_pfsubset
7 months ago, by desharna
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
7 months ago, by desharna
update components.sha1;
7 months ago, by wenzelm
proper description;
7 months ago, by wenzelm
one more lemma
7 months ago, by nipkow
merged
7 months ago, by nipkow
adjusted proofs
7 months ago, by nipkow
added and reorganized lemmas (some suggested by Jeremy Sylvestre)
7 months ago, by nipkow
removed redundant lemma
7 months ago, by nipkow
moved theorem from Fun to Set
7 months ago, by nipkow
added lemmas antisymp_ge[simp], antisymp_greater[simp], antisymp_le[simp], and antisymp_less[simp]
7 months ago, by desharna
added lemmas reflp_ge[simp] and reflp_le[simp]
7 months ago, by desharna
removed unused universal variable from lemma reflp_onI
7 months ago, by desharna
added lemmas irreflD and irreflpD
7 months ago, by desharna
added lemmas antisym_if_asym and antisymp_if_asymp
7 months ago, by desharna
strengthened lemma total_on_singleton and added lemma totalp_on_singleton
7 months ago, by desharna
generalized type classes as suggested by Jeremy Sylvestre
7 months ago, by nipkow
euclidean division on gaussian numbers
7 months ago, by haftmann
tuned proof
7 months ago, by haftmann
note on signed division on words
8 months ago, by haftmann
tuned definition
8 months ago, by haftmann
spelling
8 months ago, by haftmann
tuned proof
8 months ago, by haftmann
slightly less abusive proof pattern
8 months ago, by haftmann
back to post-release mode -- after fork point;
8 months ago, by wenzelm
Added tag Isabelle2022-RC3 for changeset d704efeb01db
8 months ago, by wenzelm
proper cygwin component (see d042947e47a3)
8 months ago, by wenzelm
proper base names;
8 months ago, by wenzelm
suppress command echo in output;
8 months ago, by wenzelm
include openssh for rsync (see also a1c7829ac2de);
8 months ago, by wenzelm
provide naproche-20221002;
8 months ago, by wenzelm
merged
8 months ago, by wenzelm
clarified signature: more operations;
8 months ago, by wenzelm
tuned signature;
8 months ago, by wenzelm
tuned, following hints by IntelliJ IDEA;
8 months ago, by wenzelm
clarified signature, to support external tools like "isabelle narration";
8 months ago, by wenzelm
syntactic type classes for signed division operators
8 months ago, by haftmann
reduce prominence of facts
8 months ago, by haftmann
clarified signature;
8 months ago, by wenzelm
more explanations on the new order prover (based on 10945fc183cd), without violating strict monotonicity of NEWS wrt. official releases;
8 months ago, by wenzelm
restore NEWS, before commit accidents 2aad8698f82f and 10945fc183cd;
8 months ago, by wenzelm
added documentation about new order prover
8 months ago, by Lukas Stevens
tweaked
8 months ago, by Lukas Stevens
tweaked;
8 months ago, by Fabian Huch
moved relevant theorems from theory Divides to theory Euclidean_Division
8 months ago, by haftmann
amend jenkins ci build;
8 months ago, by Fabian Huch
restructured ci profile into modular ci build system;
8 months ago, by Fabian Huch
more structured proofs
8 months ago, by paulson
fixed some theory presentation issues (?)
8 months ago, by paulson
recover informal "&" from 0c18df79b1c8;
8 months ago, by wenzelm
added a couple of structured proofs
8 months ago, by paulson
More obsolete "unfold" calls
8 months ago, by paulson
getting rid of apply (unfold ...)
8 months ago, by paulson
More syntactic cleanup. LaTeX markup working
8 months ago, by paulson
more modernisation of syntax
8 months ago, by paulson
Removal of obsolete ASCII syntax
8 months ago, by paulson
clarified options;
8 months ago, by wenzelm
merged
8 months ago, by wenzelm
less
more
|
(0)
-30000
-10000
-1920
tip