Tue, 01 Apr 2003 16:08:34 +0200 | ballarin | Fixed Coset.thy (proved theorem factorgroup_is_group). | file | diff | annotate |
Fri, 14 Mar 2003 18:00:16 +0100 | ballarin | Bugs fixed and operators finprod and finsum. | file | diff | annotate |
Thu, 27 Feb 2003 15:12:29 +0100 | ballarin | Change to meta simplifier: congruence rules may now have frees as head of term. | file | diff | annotate |