Sat, 21 Dec 2013 09:44:28 +0100 renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)
blanchet [Sat, 21 Dec 2013 09:44:28 +0100] rev 54842
renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)
Wed, 18 Dec 2013 11:03:40 +0100 express weak pullback property of bnfs only in terms of the relator
traytel [Wed, 18 Dec 2013 11:03:40 +0100] rev 54841
express weak pullback property of bnfs only in terms of the relator
Fri, 20 Dec 2013 21:09:01 +0100 merged
nipkow [Fri, 20 Dec 2013 21:09:01 +0100] rev 54840
merged
Fri, 20 Dec 2013 21:08:48 +0100 tuned
nipkow [Fri, 20 Dec 2013 21:08:48 +0100] rev 54839
tuned
Fri, 20 Dec 2013 20:36:38 +0100 reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)
blanchet [Fri, 20 Dec 2013 20:36:38 +0100] rev 54838
reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)
Fri, 20 Dec 2013 16:22:10 +0100 tuning whitespace
blanchet [Fri, 20 Dec 2013 16:22:10 +0100] rev 54837
tuning whitespace
Fri, 20 Dec 2013 14:27:07 +0100 recognize datatype reasoning in SPASS-Pirate
blanchet [Fri, 20 Dec 2013 14:27:07 +0100] rev 54836
recognize datatype reasoning in SPASS-Pirate
Fri, 20 Dec 2013 11:34:07 +0100 note manually proved exclusiveness property
blanchet [Fri, 20 Dec 2013 11:34:07 +0100] rev 54835
note manually proved exclusiveness property
Fri, 20 Dec 2013 11:12:51 +0100 note exhaust proof obligation
blanchet [Fri, 20 Dec 2013 11:12:51 +0100] rev 54834
note exhaust proof obligation
Fri, 20 Dec 2013 09:48:04 +0100 compile
blanchet [Fri, 20 Dec 2013 09:48:04 +0100] rev 54833
compile
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip