Nominal/nominal_function.ML
2012-10-29 Christian Urban adapted to latest change of Markus on the function package
2012-06-18 Christian Urban used ML-antiquotation command_spec for new commands
2012-04-30 Christian Urban adapted to change by Markus on function.ML
2012-03-20 Christian Urban updated to new Isabelle (20 March)
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-08-28 Christian Urban updated to Isabelle 28 Aug
2011-08-17 Christian Urban made same changes as in main branch
2011-08-15 Christian Urban uodated to new Isabelle (15. Aug)
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-16 Christian Urban added eqvt_at and invariant for boths sides of the equations
2011-06-16 Christian Urban added a test that every function must be of pt-sort
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-30 Christian Urban functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
2011-04-06 Christian Urban changed default preprocessor that does not catch variables only occuring on the right
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