Nominal/nominal_function_core.ML
2014-01-11 Christian Urban updated with current AFP version
2013-07-01 Christian Urban updated to ne Isabelle
2013-06-04 Christian Urban updated to new Isabelle
2013-04-18 Christian Urban updated to simplifier changes
2012-10-04 Christian Urban removed fork_mono flag
2012-08-07 Christian Urban definition of an auxiliary graph in nominal-primrec definitions
2012-01-16 Christian Urban updated to Isabelle 16 January
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-19 Cezary Kaliszyk Update to new Isabelle
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-22 Christian Urban some rudimentary infrastructure for storing data about nominal datatypes
2011-06-16 Christian Urban added eqvt_at and invariant for boths sides of the equations
2011-06-14 Christian Urban fixed the problem when giving a complex default-term; the fundef lemmas in Nominal_Base were not general enough
2011-06-07 Christian Urban cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
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-06-01 Christian Urban hopefully final fix for ho-functions
2011-06-01 Christian Urban first test to fix the problem with free variables
2011-05-31 Christian Urban fixed the problem with cps-like functions
2011-05-30 Christian Urban tuned last commit
2011-05-30 Christian Urban functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
2011-05-26 Christian Urban updated to new Isabelle
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-02-03 Christian Urban removed diagnostic code
2011-01-27 Christian Urban some experiments
2011-01-25 Christian Urban made eqvt-proof explicit in the function definitions
2011-01-18 Christian Urban deleted diagnostic code
2011-01-18 Christian Urban some tryes about substitution over type-schemes
2011-01-17 Christian Urban exported nominal function code to external file
less more (0) tip