QuotMain.thy
Wed, 25 Nov 2009 11:41:42 +0100 Cezary Kaliszyk Removed unused things from QuotMain.
Wed, 25 Nov 2009 10:34:03 +0100 Cezary Kaliszyk lambda_prs and cleaning the existing examples.
Wed, 25 Nov 2009 03:45:44 +0100 Christian Urban fixed the problem with generalising variables; at the moment it is quite a hack
Tue, 24 Nov 2009 19:09:29 +0100 Christian Urban changed unification to matching
Tue, 24 Nov 2009 18:13:57 +0100 Christian Urban unification
Tue, 24 Nov 2009 18:13:18 +0100 Cezary Kaliszyk Lambda & SOLVED' for new quotient_tac
Tue, 24 Nov 2009 17:35:31 +0100 Christian Urban merged
Tue, 24 Nov 2009 16:10:31 +0100 Christian Urban merged
Tue, 24 Nov 2009 15:31:29 +0100 Christian Urban use error instead of raising our own exception
Tue, 24 Nov 2009 15:18:00 +0100 Cezary Kaliszyk Fixes to the tactic after quotient_tac changed.
Tue, 24 Nov 2009 15:15:33 +0100 Christian Urban merged
Tue, 24 Nov 2009 15:15:10 +0100 Christian Urban added a prepare_tac
less more (0) -100 -12 tip