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
+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.
dropped dead code
2013-04-23, by haftmann
documentation and NEWS
2013-04-23, by haftmann
avoid accidental specialization of the types in the "map" property of codatatypes
2013-04-23, by blanchet
simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)
2013-04-23, by blanchet
more examples
2013-04-23, by blanchet
tuning
2013-04-23, by blanchet
fix bugs in expand tactic w.r.t. datatypes with "needless" discriminators (e.g. lists with is_Nil instead of ~= Nil)
2013-04-23, by blanchet
tuning
2013-04-23, by blanchet
tuned_comment
2013-04-23, by blanchet
(co)rec is (just as the (un)fold) the unique morphism;
2013-04-23, by traytel
tuned: unnamed contexts, interpretation and sublocale in locale target;
2013-04-23, by haftmann
target-sensitive user-level commands interpretation and sublocale
2013-04-23, by haftmann
ML interfaces for various kinds of interpretation
2013-04-23, by haftmann
brittleness stamping for local theories
2013-04-23, by haftmann
tuned
2013-04-23, by haftmann
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
modifiers for classical wrappers operate on Proof.context instead of claset;
2013-04-12, by wenzelm
removed historic comments;
2013-04-12, by wenzelm
tuned exceptions -- avoid composing error messages in low-level situations;
2013-04-12, by wenzelm
tuned signature;
2013-04-12, by wenzelm
proper identifiers -- avoid crash of case translations;
2013-04-12, by wenzelm
reduced duplication
2013-04-12, by nipkow
do not add case translation syntax in rep_datatype compatibility mode
2013-04-11, by traytel
run type inference on input to wrap_data
2013-04-11, by traytel
installed case translations in BNF package
2013-04-11, by traytel
tuned
2013-04-11, by nipkow
more antiquotations;
2013-04-10, by wenzelm
tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side;
2013-04-10, by wenzelm
updated keywords;
2013-04-10, by wenzelm
merged
2013-04-10, by wenzelm
merged
2013-04-10, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip