quotient.ML
Sat, 28 Nov 2009 18:49:39 +0100 Christian Urban selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
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 15:31:29 +0100 Christian Urban use error instead of raising our own exception
Mon, 23 Nov 2009 23:09:03 +0100 Christian Urban fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
Sun, 22 Nov 2009 15:30:23 +0100 Christian Urban updated to Isabelle 22nd November
Sat, 21 Nov 2009 23:23:01 +0100 Christian Urban slight tuning
Sat, 21 Nov 2009 02:49:39 +0100 Christian Urban simplified get_fun so that it uses directly rty and qty, instead of qenv
less more (0) -30 -10 -7 tip