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
+3000
+10000
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.
Quickcheck setup for finite sets
2015-07-12, by Lars Hupel
tuned proofs;
2015-07-11, by wenzelm
tuned proofs;
2015-07-11, by wenzelm
merged
2015-07-09, by wenzelm
tuned proofs;
2015-07-09, by wenzelm
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
2015-07-09, by wenzelm
clarified specific use of inspect_contract: "any Bound variable will do" may render the term invalid for Term.fastype_of1 in inst_subst_tac (see also 7c3757fccf0e);
2015-07-09, by wenzelm
tuned whitespace;
2015-07-09, by wenzelm
tuned ML signature (and rationalized code a bit)
2015-07-09, by blanchet
merged
2015-07-09, by noschinl
case_of_simps: do not split for types with a single constructor
2015-07-09, by noschinl
tests for Simps_Case_Conv
2015-07-09, by noschinl
merged
2015-07-09, by wenzelm
clarified context;
2015-07-09, by wenzelm
tuned proofs;
2015-07-09, by wenzelm
clarified context;
2015-07-09, by wenzelm
clarified context;
2015-07-08, by wenzelm
Variable.focus etc.: optional bindings provided by user;
2015-07-08, by wenzelm
clarified text folds: proof ... qed counts as extra block;
2015-07-08, by wenzelm
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
2015-07-08, by wenzelm
tuned;
2015-07-08, by wenzelm
tuned according to a81dc82ecba3;
2015-07-08, by wenzelm
tuned facts
2015-07-08, by haftmann
more cautious use of [iff] declarations
2015-07-08, by haftmann
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
2015-07-08, by haftmann
eliminated some duplication
2015-07-08, by haftmann
more algebraic properties for gcd/lcm
2015-07-08, by haftmann
moved normalization and unit_factor into Main HOL corpus
2015-07-08, by haftmann
more generous timeout for the sake of HOL-Proofs in at64-poly;
2015-07-08, by wenzelm
tuned ML signature
2015-07-07, by blanchet
have the installed termination prover take a 'quiet' flag
2015-07-07, by blanchet
add monotonicity rule for rtranclp
2015-07-07, by hoelzl
tuned proofs;
2015-07-07, by wenzelm
tuned proofs;
2015-07-06, by wenzelm
tuned proofs;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
tuned proofs;
2015-07-06, by wenzelm
tuned whitespace;
2015-07-06, by wenzelm
clarified sections;
2015-07-06, by wenzelm
clarified sections;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
clarified sections;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
tuned proofs;
2015-07-06, by wenzelm
plain string output, without funny control chars;
2015-07-06, by wenzelm
tuned message;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
proper outer syntax category, e.g. relevant for PIDE markup;
2015-07-06, by wenzelm
merged
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
clarified sections;
2015-07-06, by wenzelm
clarified section references;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
clarified sections;
2015-07-06, by wenzelm
removed outdated and mostly obsolete material;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
tuned whitespace;
2015-07-06, by wenzelm
clarified context;
2015-07-05, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
tip