Nominal/Ex/Lambda.thy
Tue, 07 Jun 2011 08:52:59 +0100 Christian Urban fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Sun, 05 Jun 2011 21:14:23 +0100 Christian Urban added an option for an invariant (at the moment only a stub)
Sat, 04 Jun 2011 09:07:50 +0900 Cezary Kaliszyk Finish and test the locale approach
Fri, 03 Jun 2011 12:46:23 +0100 Christian Urban recursion combinator inside a locale
Thu, 02 Jun 2011 22:24:33 +0900 Cezary Kaliszyk finished the missing obligations
Thu, 02 Jun 2011 12:14:03 +0100 Christian Urban merged
Thu, 02 Jun 2011 12:09:31 +0100 Christian Urban a test with a recursion combinator defined on top of nominal_primrec
less more (0) -30 -10 -7 tip