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.
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
2013-04-25, by hoelzl
renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)
2013-04-25, by hoelzl
spell conditional_ly_-complete lattices correct
2013-04-24, by hoelzl
specify nicer names for map, set and rel in the stream library
2013-04-25, by traytel
start making "wrap_data" more robust
2013-04-25, by blanchet
no eta-expansion for case in split rules and case_conv
2013-04-25, by blanchet
simplified code -- no need for two attempts, the error we get from mixfix the first time is good (and better to get than a parse error in the specification because the user tries to use a mixfix that silently failed)
2013-04-25, by blanchet
proper error generated for wrong mixfix
2013-04-24, by blanchet
honor user-specified name for relator + generalize syntax
2013-04-24, by blanchet
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
2013-04-24, by blanchet
added "fundef_cong" attribute to "map_cong"
2013-04-24, by blanchet
optimized proofs
2013-04-24, by traytel
apply arguments to f and g in "case_cong"
2013-04-24, by blanchet
derive "map_cong"
2013-04-24, by blanchet
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
2013-04-24, by blanchet
killed dead code
2013-04-24, by blanchet
eta-contracted weak congruence rules (like in the old package)
2013-04-24, by blanchet
honor user-specified name for map function
2013-04-24, by blanchet
honor user-specified set function names
2013-04-24, by blanchet
parse set function name
2013-04-24, by blanchet
merged
2013-04-24, by nipkow
tuned
2013-04-24, by nipkow
took out workaround for bug fixed in 5af40820948b
2013-04-24, by traytel
merged
2013-04-24, by traytel
slightly more aggressive syntax translation for printing case expressions
2013-04-24, by traytel
avoid odd reinit after sublocale declaration
2013-04-24, by haftmann
moved defs into locale to reduce unnecessary polymorphism; tuned
2013-04-24, by nipkow
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
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
tip