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 |
Thu, 26 Aug 2010 02:08:00 +0800 | Christian Urban | cleaned up (almost completely) the examples | file | diff | annotate |
Mon, 07 Jun 2010 11:43:01 +0200 | Christian Urban | work on transitivity proof | file | diff | annotate |