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.
helpful error message when 'auto' fails
2015-03-05, by blanchet
no quick_and_dirty for goals that may fail + tuned messages
2015-03-05, by blanchet
tuned new primrec messages
2015-03-05, by blanchet
reworked primcorec error messages
2015-03-05, by blanchet
fix import path
2015-03-05, by hoelzl
merged
2015-03-04, by wenzelm
tuned signature;
2015-03-04, by wenzelm
tuned signature;
2015-03-04, by wenzelm
removed unused;
2015-03-04, by wenzelm
merged
2015-03-04, by nipkow
Removed the obsolete functions "natfloor" and "natceiling"
2015-03-04, by nipkow
clarified signature;
2015-03-04, by wenzelm
tuned;
2015-03-04, by wenzelm
tuned;
2015-03-04, by wenzelm
merged;
2015-03-04, by wenzelm
tuned signature -- prefer qualified names;
2015-03-04, by wenzelm
alist is a BNF
2015-03-04, by traytel
eliminated some clones of Proof_Context.cterm_of
2015-03-03, by traytel
updated docs
2015-03-03, by blanchet
strengthened 'size' tactic for examples like datatype (dead 'a, 'b) y = Y "'a * 'b"
2015-03-03, by blanchet
SPASS-Pirate is now called Pirate
2015-03-03, by blanchet
avoid duplicate simp warning for datatypes with explicit products
2015-03-03, by blanchet
removed needless (and inconsistent) qualifier that messes up with Mirabelle
2015-03-03, by blanchet
import 'Main' to be on the safe side
2015-03-03, by blanchet
added Proof_Context.cterm_of/ctyp_of convenience;
2015-03-01, by wenzelm
tuned;
2015-03-01, by wenzelm
updated to jedit-5.2.0;
2015-02-28, by wenzelm
spelling
2015-02-28, by haftmann
tuned whitespace;
2015-02-27, by wenzelm
typo
2015-02-26, by nipkow
tuned;
2015-02-24, by wenzelm
updated CVC4 component to include libgmp on Mac OS X
2015-02-24, by blanchet
more uniform headless mode for all derivatives of "build" (amending df5dc24ca712);
2015-02-23, by wenzelm
Goal.prove_multi is superseded by the fully general Goal.prove_common;
2015-02-23, by wenzelm
proper LaTeX;
2015-02-23, by wenzelm
make SML/NJ more happy;
2015-02-23, by wenzelm
added new tree material
2015-02-21, by nipkow
generalised the results by Eberl
2015-02-20, by paulson
more canonical order of subscriptions avoids superfluous facts
2015-02-19, by haftmann
got rid of linordered_field_class.sign_simps(41) !
2015-02-19, by paulson
establish unique preferred fact names
2015-02-19, by haftmann
eliminated technical fact alias
2015-02-18, by haftmann
eliminated fact duplicates
2015-02-18, by haftmann
inlined rules to free user-space from technical names
2015-02-18, by haftmann
explicit declaration allows cumulative declaration
2015-02-18, by haftmann
use more permissive logic for CVC4 (in case both reals and datatypes appear)
2015-02-17, by blanchet
deleted ineffective declarations
2015-02-15, by haftmann
dropped unused rules
2015-02-15, by haftmann
more direct expression of syntactic function records
2015-02-15, by haftmann
self-contained declaration attribute
2015-02-15, by haftmann
simpset with no redundancy
2015-02-15, by haftmann
times_divide_eq rules are already [simp] despite of comment
2015-02-15, by haftmann
explicit equivalence for strict order on lattices
2015-02-15, by haftmann
tuned
2015-02-15, by haftmann
purge variables not mentioned in body from pattern
2015-02-15, by haftmann
only collapse patterns with disjunctive variable names
2015-02-14, by haftmann
clarified
2015-02-14, by haftmann
avoid unused arguments
2015-02-14, by haftmann
tuned
2015-02-14, by haftmann
more consistent teminology
2015-02-14, by haftmann
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
tip