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
-30
+30
+50
+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.
merged
2013-05-27, by wenzelm
more thorough type unification: treat equal Vars like other atoms, otherwise unify type of term pair (not just accidental body_type of its head Vars);
2013-05-27, by wenzelm
instantiate types as well (see also Thm.first_order_match);
2013-05-27, by wenzelm
tuned;
2013-05-27, by wenzelm
updated to ProofGeneral-4.2;
2013-05-27, by wenzelm
uniform Term_Position.markers (cf. dbadb4d03cbc);
2013-05-27, by wenzelm
get rid of "show_all_types" in Nitpick
2013-05-27, by blanchet
tuning
2013-05-27, by blanchet
killed dead argument
2013-05-27, by blanchet
tuning
2013-05-27, by blanchet
generalized "mk_co_iter" to handle mutualized (co)iterators
2013-05-27, by blanchet
tuning
2013-05-27, by blanchet
tuned
2013-05-27, by nipkow
tuned
2013-05-27, by nipkow
merged
2013-05-27, by nipkow
tuned
2013-05-27, by nipkow
merged
2013-05-26, by wenzelm
position constraint for bound dummy -- more PIDE markup;
2013-05-26, by wenzelm
position constraint for dummy_pattern -- more PIDE markup;
2013-05-26, by wenzelm
tuned;
2013-05-26, by wenzelm
tuned signature;
2013-05-26, by wenzelm
tuned -- less ML compiler warnings;
2013-05-26, by wenzelm
more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);
2013-05-26, by wenzelm
more uniform context;
2013-05-26, by wenzelm
tuned signature;
2013-05-26, by wenzelm
more conventional pretty printing;
2013-05-26, by wenzelm
tuned white-space;
2013-05-26, by wenzelm
more specific structure for registration into theory and dependency onto locale
2013-05-26, by haftmann
examples for interpretation into target
2013-05-26, by haftmann
disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)
2013-05-26, by blanchet
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-50
-30
+30
+50
+100
+300
+1000
+3000
+10000
tip