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 -15 +15 +100 +300 +1000 tip

proper const (see also 759bffe1d416 and b2800da9eb8a);
4 months ago, by wenzelm
tuned: inline constants;
4 months ago, by wenzelm
tuned: eliminate clone;
4 months ago, by wenzelm
tuned: more antiquotations;
4 months ago, by wenzelm
prefer host that is less likely to be down;
4 months ago, by wenzelm
adapt and activate congprocs examples, following the current Simplifier implementation;
5 months ago, by wenzelm
original Congproc_Ex.thy by Norbert Schirmer: still inactive;
5 months ago, by wenzelm
provide Simplifier.set_mksimps_context (roughly following Norbert Schirmer): allow update of context when premises are added to the local simpset;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
more direct access to Simplifier.mk_cong, to avoid odd Simpdata.mk_meta_cong seen in the wild;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
support for congprocs in the Simplifier, closely following Norbert Schirmer et-al, but with only one "simproc" name space and "simproc_setup" command / ML antiquotation;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned: anticipate congprocs;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm

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

isabelle