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.
tuned: prefer configuration options via context;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
tuned signature: more operations;
11 months ago, by wenzelm
tuned comments
11 months ago, by nipkow
merged
11 months ago, by paulson
Partial tidying of old proofs
11 months ago, by paulson
merged
11 months ago, by nipkow
new version of time_fun that works for classes; define T_length automatically now
11 months ago, by nipkow
merged
11 months ago, by paulson
revised/generalised some lemmas
11 months ago, by paulson
remove terminated jobs, even if futures do not complete;
11 months ago, by Fabian Huch
terminate jobs properly;
11 months ago, by Fabian Huch
clarified signature: eliminate clones;
11 months ago, by wenzelm
tuned: more antiquotations;
11 months ago, by wenzelm
tuned: more antiquotations;
11 months ago, by wenzelm
misc tuning;
11 months ago, by wenzelm
tuned: eliminate clone (with change of internal exceptions);
11 months ago, by wenzelm
tuned: more antiquotations;
11 months ago, by wenzelm
tuned comments and whitespace (see also 589645894305);
11 months ago, by wenzelm
tuned: more antiquotations;
11 months ago, by wenzelm
tuned: more antiquotations;
11 months ago, by wenzelm
proper const (see also 759bffe1d416 and b2800da9eb8a);
11 months ago, by wenzelm
tuned: inline constants;
11 months ago, by wenzelm
tuned: eliminate clone;
11 months ago, by wenzelm
tuned: more antiquotations;
11 months ago, by wenzelm
prefer host that is less likely to be down;
11 months ago, by wenzelm
adapt and activate congprocs examples, following the current Simplifier implementation;
11 months ago, by wenzelm
original Congproc_Ex.thy by Norbert Schirmer: still inactive;
11 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;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
more direct access to Simplifier.mk_cong, to avoid odd Simpdata.mk_meta_cong seen in the wild;
11 months ago, by wenzelm
tuned;
11 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;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
tuned: anticipate congprocs;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
tuned signature (again): anticipate different kinds of procs;
11 months ago, by wenzelm
clarified context data;
11 months ago, by wenzelm
tuned: prefer canonical argument order;
11 months ago, by wenzelm
tuned: more antiquotations;
11 months ago, by wenzelm
tuned: prefer canonical argument order;
11 months ago, by wenzelm
clarified signature: less redundant types;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
unused (see d12c58e12c51);
11 months ago, by wenzelm
tuned signature: support more general procedures;
11 months ago, by wenzelm
merged
11 months ago, by wenzelm
tuned: more antiquotations;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
tuned: more antiquotations;
11 months ago, by wenzelm
tuned whitespace;
11 months ago, by wenzelm
more robust (amending 8f53fa93d5f0): R could be anything and Thm.instantiate' involves some type-checks, e.g. relevant for lemma fset_simps in theory Quotient_Examples.Quotient_FSet;
11 months ago, by wenzelm
tuned modules;
11 months ago, by wenzelm
misc tuning;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
tuned: more antiquotations;
11 months ago, by wenzelm
misc tuning;
11 months ago, by wenzelm
misc tuning and clarification;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
misc tuning and clarification: proper context, proper exception;
11 months ago, by wenzelm
tuned: eliminate odd clones;
11 months ago, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
tip