Sat, 17 Mar 2012 05:13:59 +0000 | Christian Urban | updated to new Isabelle (declared keywords) | file | diff | annotate |
Thu, 03 Nov 2011 13:19:23 +0000 | Christian Urban | updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package | file | diff | annotate |
Tue, 05 Jul 2011 18:42:34 +0200 | Christian Urban | changed bind to binds in specifications; bind will cause trouble with Monad_Syntax | file | diff | annotate |
Tue, 03 May 2011 15:39:30 +0100 | Christian Urban | added two mutual recursive inductive definitions | file | diff | annotate |
Wed, 22 Dec 2010 09:13:25 +0000 | Christian Urban | properly exported strong exhaust theorem; cleaned up some examples | file | diff | annotate |
Sun, 29 Aug 2010 13:36:03 +0800 | Christian Urban | renamed NewParser to Nominal2 | file | diff | annotate |
Fri, 27 Aug 2010 03:37:17 +0800 | Christian Urban | "isabelle make test" makes all major examples....they work up to supp theorems (excluding) | file | diff | annotate |