20100913 
nipkow 
20100913 
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI

file  diff  annotate 
20100907 
nipkow 
20100907 
expand_fun_eq > ext_iff
expand_set_eq > set_ext_iff
Naming in line now with multisets

file  diff  annotate 
20100511 
haftmann 
20100511 
renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution

file  diff  annotate 
20100511 
haftmann 
20100511 
theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct

file  diff  annotate 
20100311 
haftmann 
20100311 
tuned prefix of ac rules

file  diff  annotate 
20100219 
haftmann 
20100219 
moved remaning class operations from Algebras.thy to Groups.thy

file  diff  annotate 
20100217 
haftmann 
20100217 
added simple theory about discrete summation

file  diff  annotate 