isabelle: Changelog

haftmann [Sat, 28 Apr 2012 10:03:46 +0200] rev 47820

less confusion in NEWS

haftmann [Sat, 28 Apr 2012 09:55:01 +0200] rev 47819

rhs of abstract code equations are not subject to preprocessing: inline code abbrevs explicitly

nipkow [Sat, 28 Apr 2012 07:38:22 +0200] rev 47818

renamed Semi to Seq

wenzelm [Fri, 27 Apr 2012 23:17:58 +0200] rev 47817

merged

wenzelm [Fri, 27 Apr 2012 22:58:29 +0200] rev 47816

prefer Context_Position.report_generic, which observes is_visible flag and thus reduces number of echos;

wenzelm [Fri, 27 Apr 2012 22:47:30 +0200] rev 47815

clarified signature;

wenzelm [Fri, 27 Apr 2012 21:47:47 +0200] rev 47814

avoid spurious warning in invisible context, notably Haftmann-Wenzel sandwich;

wenzelm [Fri, 27 Apr 2012 21:44:44 +0200] rev 47813

made Context_Position independent from Config;

blanchet [Fri, 27 Apr 2012 22:36:27 +0200] rev 47812

use Nitpick as an oracle for finite problems

blanchet [Fri, 27 Apr 2012 22:36:27 +0200] rev 47811

add extensionality to first-order provers

isabelle