isabelle: Changelog

blanchet [Thu, 24 Oct 2013 15:32:34 +0200] rev 54198

got rid of annoying duplicate rewrite rule warnings

blanchet [Thu, 24 Oct 2013 12:43:33 +0200] rev 54197

use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations

traytel [Thu, 24 Oct 2013 10:03:20 +0200] rev 54196

refactored rtrancl_while; prove termination for finite rtrancl

nipkow [Wed, 23 Oct 2013 21:12:20 +0200] rev 54195

more exercises

nipkow [Wed, 23 Oct 2013 18:04:43 +0200] rev 54194

added exercises

blanchet [Wed, 23 Oct 2013 14:53:36 +0200] rev 54193

added 'primcorec' examples

nipkow [Wed, 23 Oct 2013 09:58:30 +0200] rev 54192

tuned

traytel [Tue, 22 Oct 2013 16:07:09 +0200] rev 54191

removed junk

traytel [Tue, 22 Oct 2013 14:22:06 +0200] rev 54190

update doc according to c0186a0d8cb3

traytel [Tue, 22 Oct 2013 14:17:12 +0200] rev 54189

define a trivial nonemptiness witness if none is provided

isabelle