| 2009-12-30 | cu | some small changes | file | diff | annotate |
| 2009-12-27 | Christian Urban | added a functor that allows checking what is added to the theorem lists | file | diff | annotate |
| 2009-12-26 | Christian Urban | corrected wrong [quot_respect] attribute; tuned | file | diff | annotate |
| 2009-12-26 | Christian Urban | added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML) | file | diff | annotate |
| 2009-12-26 | Christian Urban | as expected problems occure when lifting concat lemmas | file | diff | annotate |
| 2009-12-24 | Christian Urban | made the quotient_type definition more like typedef; now type variables need to be explicitly given | file | diff | annotate |
| 2009-12-23 | Christian Urban | renamed some fields in the info records | file | diff | annotate |