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
+30000
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.
removed type constraints
2013-04-22, by immler
NEWS
2013-04-22, by hoelzl
more sharing
2013-04-21, by haftmann
interpretation: distinguish theories and proofs by explicit parameter rather than generic context;
2013-04-21, by haftmann
dropped unusued identifier
2013-04-21, by haftmann
avoid odd bifurcation with Attrib.local_notes vs. Locale.add_thmss -- n.b. note_eqns_dependency operates in a specific locale target
2013-04-21, by haftmann
tuned for uniformity
2013-04-21, by haftmann
reflection as official HOL tool
2013-04-21, by haftmann
follow Isabelle spacing praxis more thoroughly
2013-04-21, by haftmann
honour FIXMEs as far as feasible at the moment
2013-04-21, by haftmann
combined reify_data.ML into reflection.ML;
2013-04-21, by haftmann
proved termination for fun-based AI
2013-04-20, by nipkow
tuned
2013-04-20, by nipkow
tuned
2013-04-19, by nipkow
merged
2013-04-18, by wenzelm
tuned signature;
2013-04-18, by wenzelm
simplifier uses proper Proof.context instead of historic type simpset;
2013-04-18, by wenzelm
merged
2013-04-18, by nipkow
avoided map_of in def of fun_rep (but still needed for efficient code)
2013-04-18, by nipkow
spelling
2013-04-18, by haftmann
spelling
2013-04-18, by haftmann
tuned
2013-04-17, by nipkow
complete revision: finally got rid of annoying L-predicate
2013-04-17, by nipkow
moved leastness lemma
2013-04-17, by nipkow
proper prolog command-line instead of hashbang, which might switch to invalid executable and thus fail (notably on lxbroy2);
2013-04-16, by wenzelm
use automatic type coerctions in Sqrt example
2013-04-15, by hoelzl
make SML/NJ happy;
2013-04-15, by wenzelm
not all Nitpick 'constructors' are injective -- careful
2013-04-15, by blanchet
added another definition snipped
2013-04-14, by kleing
actually fail on prolog errors -- such as swipl startup failure due to missing shared libraries -- assuming it normally produces clean return code 0;
2013-04-12, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-50
-30
+30
+50
+100
+300
+1000
+3000
+10000
+30000
tip