isabelle: Changelog

blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57749

reorder quantifiers to ease Z3 skolemization

blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57748

tuned order of arguments

blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57747

tuned name context code

blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57746

tuned whitespace

blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57745

more rational unskolemizing of names

blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57744

added appropriate method for skolemization of Z3 steps to the mix

blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57743

pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)

blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57742

honor 'try0' also for one-liners

blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57741

tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence

blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57740

further minimize one-liner

isabelle