Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
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.
support incremental isabelle.select-structure --- like select-block, but based on selection instead of caret;
11 months ago, by wenzelm
clarified rendering: entity acts as atomic notation / expression;
11 months ago, by wenzelm
more rendering for Markup.COMMAND_SPAN, following Rendering.structure_elements;
11 months ago, by wenzelm
more NEWS;
11 months ago, by wenzelm
merged
11 months ago, by wenzelm
support Isabelle/jEdit action isabelle.select_structure;
11 months ago, by wenzelm
more operations;
11 months ago, by wenzelm
clarified text;
11 months ago, by wenzelm
update to jedit5.7.0;
11 months ago, by wenzelm
GUI option "editor_auto_hovering" for Output panel;
11 months ago, by wenzelm
update to scala-3.3.4 LTS;
11 months ago, by wenzelm
removed obsolete markup for "open_block" (see also d5ad89fda714): Isabelle/Scala directly supports XML.Elem pretty-printing;
11 months ago, by wenzelm
Library material from Eberl's Parallel_Shear_Sort
11 months ago, by paulson
Trying to clean up these horribly ugly old proofs, but the requirement of constructivity makes it very difficult
11 months ago, by paulson
use automatically generated time function in HOL-Data_Structures.Selection
11 months ago, by Manuel Eberl
merged
11 months ago, by nipkow
better time_functions (let)
11 months ago, by nipkow
less hidden configuration;
11 months ago, by Fabian Huch
proper passwordless smtp check: must be null;
11 months ago, by Fabian Huch
adjusted documentation
11 months ago, by blanchet
more attribute tuning
11 months ago, by nipkow
tuned attributes
11 months ago, by nipkow
merged
11 months ago, by nipkow
added lemmas
11 months ago, by nipkow
tuned proofs;
11 months ago, by wenzelm
tuned NEWS;
11 months ago, by wenzelm
markup for "..." notation;
11 months ago, by wenzelm
more robust: avoid non-authentic translations;
11 months ago, by wenzelm
tuned whitespace of sources;
11 months ago, by wenzelm
update documentation;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
update documentation: print mode "latex" only affects syntax tables, but output of symbols;
11 months ago, by wenzelm
misc tuning and clarification;
11 months ago, by wenzelm
clarified section structure;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
tuned signature;
11 months ago, by wenzelm
clarified symbolic output: avoid redundant "block" element for open_block = true;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
clarified (again): Markup.intensify is already part of Variable.markup_fixed for undeclared variable, Markup.fixed is already part of Mariable.markup;
11 months ago, by wenzelm
more accurate Symbol.length;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
merged
11 months ago, by wenzelm
more inner-syntax markup;
11 months ago, by wenzelm
obsolete (see a8502d492dde);
11 months ago, by wenzelm
minor performance tuning;
11 months ago, by wenzelm
tuned proofs;
11 months ago, by wenzelm
more inner-syntax markup;
11 months ago, by wenzelm
merged
11 months ago, by nipkow
time_fun: lambdas and lets work now
11 months ago, by nipkow
variable instantiation in Sledgehammer and Metis
11 months ago, by blanchet
prefer rewrite_term_yoyo for improved performance and occasionally better results (conforming to Ast.normalize);
11 months ago, by wenzelm
revert b35c2aa05fcf: redundant due to 89ea66c2045b, if object-logic judgment lacks delimiters;
11 months ago, by wenzelm
clarified position constraints: omit redundant information, e.g. for implicit object-logic judgment;
11 months ago, by wenzelm
unused (see 0199acc01aa8);
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
more robust: avoid ambiguity of contract_abbrevs;
11 months ago, by wenzelm
misc tuning: more concise (or hermetic) pointfree style;
11 months ago, by wenzelm
provide rewrite_term_yoyo, which is analogous to Ast.normalize;
11 months ago, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
tip