isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -50 -24 +24 +50 +100 +300 tip

variable instantiation in Sledgehammer and Metis
3 months ago, by blanchet
prefer rewrite_term_yoyo for improved performance and occasionally better results (conforming to Ast.normalize);
3 months ago, by wenzelm
revert b35c2aa05fcf: redundant due to 89ea66c2045b, if object-logic judgment lacks delimiters;
3 months ago, by wenzelm
clarified position constraints: omit redundant information, e.g. for implicit object-logic judgment;
3 months ago, by wenzelm
unused (see 0199acc01aa8);
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more robust: avoid ambiguity of contract_abbrevs;
3 months ago, by wenzelm
misc tuning: more concise (or hermetic) pointfree style;
3 months ago, by wenzelm
provide rewrite_term_yoyo, which is analogous to Ast.normalize;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned names;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
misc tuning and clarification;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
misc tuning and clarification;
3 months ago, by wenzelm
merged
3 months ago, by wenzelm
adhoc option to disable const constraints, notably for AFP/Isabelle_DOF;
3 months ago, by wenzelm
unused;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
proper treatment of position constraints;
3 months ago, by wenzelm
more liberal ast matching, notably for case-translations in HOLCF that operate on logical consts rather than syntax consts;
3 months ago, by wenzelm
more parser markup, based on position constraints for logical mixfix syntax;
3 months ago, by wenzelm
more concise representation of term positions;
3 months ago, by wenzelm
more robust;
3 months ago, by wenzelm

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -50 -24 +24 +50 +100 +300 tip

isabelle