isabelle: Changelog

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

modernized Mirabelle (a bit) and made it compile

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

restored a bit of laziness

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

isabelle