2013-04-26 blanchet 2013-04-26 more intuitive syntax for equality-style discriminators of nullary constructors
2013-04-26 blanchet 2013-04-26 updated keywords
2013-04-26 blanchet 2013-04-26 put an underscore in prefix
2013-04-26 blanchet 2013-04-26 changed discriminator default: avoid mixing ctor and dtor views
2013-04-26 nipkow 2013-04-26 simplified def
2013-04-26 nipkow 2013-04-26 more standard order of arguments
2013-04-26 nipkow 2013-04-26 more funs
2013-04-26 nipkow 2013-04-26 simplified def
2013-04-25 traytel 2013-04-25 removed unnecessary assumptions in some theorems about cardinal exponentiation
2013-04-25 blanchet 2013-04-25 renamed "wrap_data" to "wrap_free_constructors"
2013-04-25 blanchet 2013-04-25 register coinductive type's coinduct rule
2013-04-25 blanchet 2013-04-25 compile
2013-04-25 blanchet 2013-04-25 adjusted stream library to coinduct attributes
2013-04-25 blanchet 2013-04-25 generate proper attributes for coinduction rules
2013-04-25 wenzelm 2013-04-25 updated to jdk-7u21;
2013-04-25 hoelzl 2013-04-25 revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
2013-04-25 hoelzl 2013-04-25 renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)
2013-04-24 hoelzl 2013-04-24 spell conditional_ly_-complete lattices correct
2013-04-25 traytel 2013-04-25 specify nicer names for map, set and rel in the stream library
2013-04-25 blanchet 2013-04-25 start making "wrap_data" more robust
2013-04-25 blanchet 2013-04-25 no eta-expansion for case in split rules and case_conv
2013-04-25 blanchet 2013-04-25 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-24 blanchet 2013-04-24 proper error generated for wrong mixfix
2013-04-24 blanchet 2013-04-24 honor user-specified name for relator + generalize syntax
2013-04-24 blanchet 2013-04-24 renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
2013-04-24 blanchet 2013-04-24 added "fundef_cong" attribute to "map_cong"
2013-04-24 traytel 2013-04-24 optimized proofs
2013-04-24 blanchet 2013-04-24 apply arguments to f and g in "case_cong"
2013-04-24 blanchet 2013-04-24 derive "map_cong"
2013-04-24 blanchet 2013-04-24 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
2013-04-24 blanchet 2013-04-24 killed dead code
2013-04-24 blanchet 2013-04-24 eta-contracted weak congruence rules (like in the old package)
2013-04-24 blanchet 2013-04-24 honor user-specified name for map function
2013-04-24 blanchet 2013-04-24 honor user-specified set function names
2013-04-24 blanchet 2013-04-24 parse set function name
2013-04-24 nipkow 2013-04-24 merged
2013-04-24 nipkow 2013-04-24 tuned
2013-04-24 traytel 2013-04-24 took out workaround for bug fixed in 5af40820948b
2013-04-24 traytel 2013-04-24 merged
2013-04-24 traytel 2013-04-24 slightly more aggressive syntax translation for printing case expressions
2013-04-24 haftmann 2013-04-24 avoid odd reinit after sublocale declaration
2013-04-24 nipkow 2013-04-24 moved defs into locale to reduce unnecessary polymorphism; tuned
2013-04-23 haftmann 2013-04-23 dropped dead code
2013-04-23 haftmann 2013-04-23 documentation and NEWS
2013-04-23 blanchet 2013-04-23 avoid accidental specialization of the types in the "map" property of codatatypes
2013-04-23 blanchet 2013-04-23 simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)
2013-04-23 blanchet 2013-04-23 more examples
2013-04-23 blanchet 2013-04-23 tuning
2013-04-23 blanchet 2013-04-23 fix bugs in expand tactic w.r.t. datatypes with "needless" discriminators (e.g. lists with is_Nil instead of ~= Nil)
2013-04-23 blanchet 2013-04-23 tuning
2013-04-23 blanchet 2013-04-23 tuned_comment
2013-04-23 traytel 2013-04-23 (co)rec is (just as the (un)fold) the unique morphism;
2013-04-23 haftmann 2013-04-23 tuned: unnamed contexts, interpretation and sublocale in locale target; corrected slip in List.thy: setsum requires commmutativity
2013-04-23 haftmann 2013-04-23 target-sensitive user-level commands interpretation and sublocale
2013-04-23 haftmann 2013-04-23 ML interfaces for various kinds of interpretation
2013-04-23 haftmann 2013-04-23 brittleness stamping for local theories
2013-04-23 haftmann 2013-04-23 tuned
2013-04-22 immler 2013-04-22 removed type constraints
2013-04-22 hoelzl 2013-04-22 NEWS
2013-04-21 haftmann 2013-04-21 more sharing