isabelle: Changelog

traytel [Wed, 08 May 2013 13:33:04 +0200] rev 51918

relator induction for datatypes

traytel [Wed, 08 May 2013 11:57:42 +0200] rev 51917

store proper theorems even for fixed points that have no passive live variables

traytel [Wed, 08 May 2013 09:45:30 +0200] rev 51916

stronger monotonicity property for relators

traytel [Wed, 08 May 2013 09:39:30 +0200] rev 51915

make tactic actually work for op = as relator

nipkow [Wed, 08 May 2013 06:14:11 +0200] rev 51914

tuned

nipkow [Wed, 08 May 2013 04:16:44 +0200] rev 51913

hide Fin on output

blanchet [Tue, 07 May 2013 21:37:40 +0200] rev 51912

removed dead argument

blanchet [Tue, 07 May 2013 21:09:47 +0200] rev 51911

more robust iterator construction (needed for mutualized FPs)

blanchet [Tue, 07 May 2013 21:09:46 +0200] rev 51910

tuning

traytel [Tue, 07 May 2013 18:40:23 +0200] rev 51909

removed dead internal constants/theorems

isabelle