Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
tuned;
16 months ago, by wenzelm
tunes signature;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
more systematic Sessions.illegal_theory, based on File_Format.theory_excluded;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
unused;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
clarified modules;
16 months ago, by wenzelm
tuned: no need to map master_dir, which does not participate in comparison;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
tuned comments;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
removed an unfortunate sledgehammer command
16 months ago, by paulson
A couple of patches
16 months ago, by paulson
Big simplifications of old proofs
16 months ago, by paulson
repaired a proof
16 months ago, by paulson
Continued proof simplifications
16 months ago, by paulson
merged
16 months ago, by paulson
A further round of proof consolidation
16 months ago, by paulson
tuned signature: avoid too many aliases;
16 months ago, by wenzelm
proper thread context (amending 01a7265db76b) -- at the danger of blocking the GUI;
16 months ago, by wenzelm
more robust: avoid detour via somewhat fragile Node.Name.path;
16 months ago, by wenzelm
clarified generic path operations;
16 months ago, by wenzelm
more flexible: implicit support for Windows;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
clarified output;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
merged
16 months ago, by paulson
More tidying
16 months ago, by paulson
Further cleaning up of messy proofs
16 months ago, by paulson
merged
16 months ago, by paulson
reorganisation and simplification of theorems about transcendental functions
16 months ago, by paulson
tuned signature;
16 months ago, by wenzelm
support asynchronous presentation commands, but not for "no_update" / "Keep", which is usually forked via "Toplevel.diag";
16 months ago, by wenzelm
tuned whitespace;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
discontinued somewhat pointless exception FAILURE with its "alt_state", which was originally due to quasi-mutable states (see 169e5b07ec06);
16 months ago, by wenzelm
tuned --- more robust ML patterns;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
merged
16 months ago, by wenzelm
tuned signature, for the sake of AFP/Isabelle_C;
16 months ago, by wenzelm
more uniform report of Markup.language_path;
16 months ago, by wenzelm
omit pointless guard: ultimately observed by Isabelle_Process.report_message;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
clarified modules;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned output;
16 months ago, by wenzelm
merged
16 months ago, by paulson
Tidied some messy proofs
16 months ago, by paulson
merged
16 months ago, by wenzelm
clarified modules: avoid duplication;
16 months ago, by wenzelm
tuned output;
16 months ago, by wenzelm
support for generic File_Format.parse_data, with persistent result in document model;
16 months ago, by wenzelm
omit warning: somewhat pointless and out-of-context;
16 months ago, by wenzelm
clarified signature: avoid case class with mutable state;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
clarified signature: more explicit types;
16 months ago, by wenzelm
merged
16 months ago, by paulson
tidied some messy old proofs
16 months ago, by paulson
tuned signature;
16 months ago, by wenzelm
merged
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
more robust;
16 months ago, by wenzelm
clarified signature: more position information via node_name;
16 months ago, by wenzelm
tuned signature: avoid name confusion;
16 months ago, by wenzelm
more bibtex errors;
16 months ago, by wenzelm
clarified signature: internalize errors (but: the parser rarely fails);
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
clarified signature: more explicit types;
16 months ago, by wenzelm
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
16 months ago, by wenzelm
merged
16 months ago, by desharna
removed old lemma names
16 months ago, by desharna
merged
16 months ago, by paulson
merged
16 months ago, by paulson
A few new Sup/Inf lemmas
16 months ago, by paulson
clarified messages;
16 months ago, by wenzelm
tuned signature: follow terminology of VSCode_Resources;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
16 months ago, by wenzelm
update URL;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
clarified signature: more explicit types;
16 months ago, by wenzelm
merged
16 months ago, by desharna
merged
16 months ago, by desharna
used transp_on in assumptions of lemmas Multiset.bex_(least|greatest)_element
16 months ago, by desharna
added lemma trans_on_lex_prod[simp]
16 months ago, by desharna
strengthened and renamed lemma trans_converse and added lemma transp_on_conversep
16 months ago, by desharna
strengthened and renamed trans_reflclI
16 months ago, by desharna
strengthened and renamed transp_reflclp
16 months ago, by desharna
strengthened and renamed lemmas preorder.transp_(ge|gr|le|less)
16 months ago, by desharna
added lemmas trans_on_subset and transp_on_subset
16 months ago, by desharna
added lemmas trans_onD and transp_onD
16 months ago, by desharna
added lemmas trans_onI and transp_onI
16 months ago, by desharna
added lemma transp_on_trans_on_eq[pred_set_conv]
16 months ago, by desharna
fixed code-generation failure
16 months ago, by desharna
added predicates trans_on and transp_on and redefined trans and transp to be abbreviations
16 months ago, by desharna
only show sessions with document setup;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
proper node name instead of not base tex_name (amending 2fd0c33fe440);
16 months ago, by wenzelm
proper migrate_name between different kinds of Resources, notably for Windows;
16 months ago, by wenzelm
merged
16 months ago, by desharna
added lemmas irrefl_on_if_asym_on[simp] and irreflp_on_if_asymp_on[simp]
16 months ago, by desharna
proper PIDE session background for interactive document context;
16 months ago, by wenzelm
NEWS;
16 months ago, by wenzelm
more accurate error messages;
16 months ago, by wenzelm
merged
16 months ago, by wenzelm
actually build document;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
tuned comments;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
clarified GUI;
16 months ago, by wenzelm
more thorough GUI updates, notably for multiple Document dockables;
16 months ago, by wenzelm
Additional new material about infinite products, etc.
16 months ago, by paulson
merged
16 months ago, by paulson
First round of moving material from the number theory development
16 months ago, by paulson
merged
16 months ago, by wenzelm
more GUI operations;
16 months ago, by wenzelm
proper handling of state updates;
16 months ago, by wenzelm
clarified process management;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
clarified state document nodes for Theories_Status / Document_Dockable;
16 months ago, by wenzelm
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
16 months ago, by wenzelm
tuned whitespace;
16 months ago, by wenzelm
clarified module initialization;
16 months ago, by wenzelm
tuned signature, following Document_Dockable;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
clarified GUI;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
proper thread context;
16 months ago, by wenzelm
more informative errors, including optional Exn.trace;
16 months ago, by wenzelm
clarified state change: presumably more robust;
16 months ago, by wenzelm
proper state change, e.g. on open/close of "Document" panel;
16 months ago, by wenzelm
clarified module initialization;
16 months ago, by wenzelm
clarified state: node_required is guarded by PIDE.editor.document_active (e.g. open panel);
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
added lifting_forget as suggested by Peter Lammich
16 months ago, by blanchet
merged
16 months ago, by desharna
added lemma refl_lex_prod[simp]
16 months ago, by desharna
added lemmas reflI and reflD
16 months ago, by desharna
added lemmas asym_on_lex_prod[simp] and asym_lex_prod[simp]
16 months ago, by desharna
added lemmas sym_on_lex_prod[simp] and sym_lex_prod[simp]
16 months ago, by desharna
added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp]
16 months ago, by desharna
strengthened and renamed lemmas asym_if_irrefl_and_trans and asymp_if_irreflp_and_transp
16 months ago, by desharna
strengthened and renamed lemma antisym_converse and added lemma antisymp_on_conversep
16 months ago, by desharna
added lemmas asym_on_converse[simp] and asymp_on_conversep[simp]
16 months ago, by desharna
strengthened and renamed lemma sym_converse and added lemma symp_on_conversep
16 months ago, by desharna
strengthened and renamed lemmas antisymp_less and antisymp_greater
16 months ago, by desharna
strengthened lemmas antisym_on_if_asym_on and antisymp_on_if_asymp_on
16 months ago, by desharna
tuned naming
16 months ago, by desharna
added lemma asymp_on_asym_on_eq[pred_set_conv]
16 months ago, by desharna
strengthened and renamed asymp_less and asymp_greater
16 months ago, by desharna
added lemmas asym_on_subset and asymp_on_subset
16 months ago, by desharna
added lemmas asym_onI, asymp_onI, asym_onD, and asymp_onD
16 months ago, by desharna
added predicates asym_on and asymp_on and redefined asym and asymp to be abbreviations
16 months ago, by desharna
clarified state and process;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
merged
16 months ago, by desharna
strengthened and renamed symp_symclp
16 months ago, by desharna
merged
16 months ago, by nipkow
Tuned text
16 months ago, by nipkow
clarified signature: avoid confusion due to redundant standard_path, which is already used here (but not elsewhere);
16 months ago, by wenzelm
clarified signature: avoid case class with redefined equality;
16 months ago, by wenzelm
discontinued somewhat pointless dependency: avoid illusion of extra accuracy (see also 09fb749d1a1e and 0f750a6dc754);
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
unused;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned whitespace;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
tuned output;
16 months ago, by wenzelm
prefer SML here
16 months ago, by haftmann
Typo.
16 months ago, by haftmann
merged
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified names;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
tuned signature (see also 8342cba8eae8);
16 months ago, by wenzelm
tuned names: avoid overlap with instances of class Resources;
16 months ago, by wenzelm
merged
16 months ago, by nipkow
file with partial function docu
16 months ago, by nipkow
Added section about code generation for partial functions
16 months ago, by nipkow
added lemmas sym_on_subset and symp_on_subset
16 months ago, by desharna
added lemmas sym_onD and symp_onD
16 months ago, by desharna
added lemmas sym_onI and symp_onI
16 months ago, by desharna
added lemma symp_on_sym_on_eq[pred_set_conv]
16 months ago, by desharna
added predicates sym_on and symp_on and redefined sym and symp to be abbreviations
16 months ago, by desharna
added lemmas IMGU_subst_domain_subset and IMGU_range_vars_subset
16 months ago, by desharna
added lemmas antisym_on_subset and antisymp_on_subset
16 months ago, by desharna
strengthened antisymp_le and antisymp_ge
16 months ago, by desharna
added lemmas antisym_onD and antisymp_onD
16 months ago, by desharna
added lemmas antisym_onI and antisymp_onI
16 months ago, by desharna
added lemma antisymp_reflcp
16 months ago, by desharna
added antisymp_on_antisym_on_eq[pred_set_conv]
16 months ago, by desharna
added predicates antisym_on and antisymp_on and redefined antisym and antisymp to be abbreviations
16 months ago, by desharna
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
clarified order: accumulate strictly from left to right;
16 months ago, by wenzelm
clarified modules;
16 months ago, by wenzelm
clarified modules;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
clarified signature: more types and operations;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
proper file extension for Isabelle_System.extract;
16 months ago, by wenzelm
tuned implementation;
16 months ago, by wenzelm
more uniform use of make_directory;
16 months ago, by wenzelm
tuned message;
16 months ago, by wenzelm
tuned: less redundant implementation;
16 months ago, by wenzelm
clarified signature: copy directory content more directly;
16 months ago, by wenzelm
more robust;
16 months ago, by wenzelm
tuned whitespace;
16 months ago, by wenzelm
clarified signature: more general operations;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
tip