Christian Urban <urbanc@in.tum.de> [Wed, 23 Dec 2009 13:23:33 +0100] rev 780
explicit handling of mem_def, avoiding the use of the simplifier; this fixes some quotient_type definitions
Christian Urban <urbanc@in.tum.de> [Wed, 23 Dec 2009 10:31:54 +0100] rev 779
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de> [Tue, 22 Dec 2009 22:10:48 +0100] rev 778
added "Highest Priority" category; and tuned slightly code
Christian Urban <urbanc@in.tum.de> [Tue, 22 Dec 2009 21:44:50 +0100] rev 777
added a print_maps command; updated the keyword file accordingly
Christian Urban <urbanc@in.tum.de> [Tue, 22 Dec 2009 21:31:44 +0100] rev 776
renamed get_fun to absrep_fun; introduced explicit checked versions of the term functions
Christian Urban <urbanc@in.tum.de> [Tue, 22 Dec 2009 21:16:11 +0100] rev 775
tuned
Christian Urban <urbanc@in.tum.de> [Tue, 22 Dec 2009 21:06:46 +0100] rev 774
moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de> [Tue, 22 Dec 2009 20:51:37 +0100] rev 773
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de> [Tue, 22 Dec 2009 07:42:16 +0100] rev 772
on the hunt for what condition raises which exception in the CLEVER CODE of calculate_inst
Christian Urban <urbanc@in.tum.de> [Tue, 22 Dec 2009 07:28:09 +0100] rev 771
simplified calculate_instance; worked around some clever code; clever code is unfortunately still there...needs to be removed