register coinductive type's coinduct rule

compile

adjusted stream library to coinduct attributes

generate proper attributes for coinduction rules

updated to jdk-7u21;

revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space

renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)

spell conditional_ly_-complete lattices correct

specify nicer names for map, set and rel in the stream library

start making "wrap_data" more robust

no eta-expansion for case in split rules and case_conv

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)

proper error generated for wrong mixfix

honor user-specified name for relator + generalize syntax

renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus

added "fundef_cong" attribute to "map_cong"

optimized proofs

apply arguments to f and g in "case_cong"

derive "map_cong"

renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"

killed dead code

eta-contracted weak congruence rules (like in the old package)

honor user-specified name for map function

honor user-specified set function names

parse set function name

merged

tuned

took out workaround for bug fixed in 5af40820948b

merged

slightly more aggressive syntax translation for printing case expressions

avoid odd reinit after sublocale declaration

moved defs into locale to reduce unnecessary polymorphism; tuned