Nominal/nominal_mutual.ML
2013-06-04 Christian Urban updated to new Isabelle
2013-04-18 Christian Urban updated to simplifier changes
2012-11-29 Christian Urban fixed problem with not fresh enough permutation name in nominal_primrec
2012-08-07 Christian Urban definition of an auxiliary graph in nominal-primrec definitions
2011-11-03 Christian Urban updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package
2011-07-22 Christian Urban tuned
2011-07-22 Christian Urban completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list
2011-07-19 Christian Urban temporary fix
2011-07-19 Christian Urban merged
2011-07-19 Christian Urban preliminary version of automatically generation the eqvt-lemmas for functions defined with nominal_primrec
2011-07-19 Christian Urban generated the partial eqvt-theorem for functions
2011-07-18 Christian Urban added a flag (eqvt) to termination proofs arising fron nominal_primrecs
2011-06-07 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
2011-06-05 Christian Urban added an option for an invariant (at the moment only a stub)
2011-05-10 Christian Urban updated to new Isabelle (> 9 May)
2011-03-16 Christian Urban ported changes from function package....needs Isabelle 16 March or above
2011-01-17 Christian Urban exported nominal function code to external file
less more (0) tip