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
blanchet [Fri, 20 Dec 2013 11:34:07 +0100] rev 54835
note manually proved exclusiveness property
blanchet [Fri, 20 Dec 2013 11:12:51 +0100] rev 54834
note exhaust proof obligation
blanchet [Fri, 20 Dec 2013 09:48:04 +0100] rev 54833
compile
blanchet [Thu, 19 Dec 2013 21:49:30 +0100] rev 54832
implemented 'exhaustive' option in tactic
blanchet [Thu, 19 Dec 2013 20:07:06 +0100] rev 54831
tuning
blanchet [Thu, 19 Dec 2013 19:37:43 +0100] rev 54830
tuning
blanchet [Thu, 19 Dec 2013 19:35:50 +0100] rev 54829
tuning 'case' expressions
blanchet [Thu, 19 Dec 2013 19:16:44 +0100] rev 54828
don't do 'isar_try0' if preplaying is off
blanchet [Thu, 19 Dec 2013 18:39:54 +0100] rev 54827
more data structure refactoring
blanchet [Thu, 19 Dec 2013 18:22:31 +0100] rev 54826
data structure rationalization