Mon, 16 Jan 2012 12:42:47 +0000 | Christian Urban | updated to Isabelle 16 January | 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 |
Fri, 19 Aug 2011 10:56:12 +0900 | Cezary Kaliszyk | Update to new Isabelle | file | diff | annotate |
Tue, 19 Jul 2011 01:40:36 +0100 | Christian Urban | generated the partial eqvt-theorem for functions | file | diff | annotate |
Mon, 18 Jul 2011 17:40:13 +0100 | Christian Urban | added a flag (eqvt) to termination proofs arising fron nominal_primrecs | file | diff | annotate |
Wed, 22 Jun 2011 12:18:22 +0100 | Christian Urban | some rudimentary infrastructure for storing data about nominal datatypes | file | diff | annotate |
Thu, 16 Jun 2011 13:14:16 +0100 | Christian Urban | added eqvt_at and invariant for boths sides of the equations | file | diff | annotate |