panny [Mon, 23 Dec 2013 15:30:31 +0100] rev 54851
prevent ambiguity when mutual recursion maps a datatype to itself, which yielded wrong definitions in some cases (e.g. nat)
haftmann [Mon, 23 Dec 2013 16:16:36 +0100] rev 54850
NEWS
haftmann [Mon, 23 Dec 2013 14:24:22 +0100] rev 54849
dropped redundant lemma
haftmann [Mon, 23 Dec 2013 14:24:21 +0100] rev 54848
syntactically tuned
haftmann [Mon, 23 Dec 2013 14:24:20 +0100] rev 54847
prefer plain bool over dedicated type for binary digits
nipkow [Mon, 23 Dec 2013 09:21:38 +0100] rev 54846
tuned
blanchet [Sat, 21 Dec 2013 09:44:30 +0100] rev 54845
compile + reduce problem size by a notch
blanchet [Sat, 21 Dec 2013 09:44:30 +0100] rev 54844
generate exhaust from nchotomy
blanchet [Sat, 21 Dec 2013 09:44:29 +0100] rev 54843
made tactic work with theorems with multiple assumptions
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)
traytel [Wed, 18 Dec 2013 11:03:40 +0100] rev 54841
express weak pullback property of bnfs only in terms of the relator
nipkow [Fri, 20 Dec 2013 21:09:01 +0100] rev 54840
merged
nipkow [Fri, 20 Dec 2013 21:08:48 +0100] rev 54839
tuned
blanchet [Fri, 20 Dec 2013 20:36:38 +0100] rev 54838
reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)
blanchet [Fri, 20 Dec 2013 16:22:10 +0100] rev 54837
tuning whitespace
blanchet [Fri, 20 Dec 2013 14:27:07 +0100] rev 54836
recognize datatype reasoning in SPASS-Pirate