Nominal/nominal_library.ML
2011-12-13 Christian Urban updated to Isabelle 13 Dec
2011-11-26 Christian Urban used simproc-antiquotation
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 completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list
2011-06-22 Christian Urban tuned
2011-06-22 Christian Urban deleted some dead code
2011-06-16 Christian Urban got rid of the boolean flag in the raw_equivariance function
2011-02-28 Christian Urban split the library into a basics file; merged Nominal_Eqvt into Nominal_Base
2011-01-06 Christian Urban removed debugging code abd introduced a guarded tracing function
2011-01-04 Christian Urban final version of the ESOP paper; used set+ instead of res as requested by one reviewer
2011-01-03 Christian Urban simple cases for string rule inductions
2010-12-28 Christian Urban automated all strong induction lemmas
2010-12-23 Christian Urban moved generic functions into nominal_library
2010-12-22 Christian Urban updated to Isabelle 22 December
2010-12-22 Christian Urban a bit tuning
2010-12-21 Christian Urban all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
2010-12-17 Christian Urban tuned
2010-12-16 Christian Urban simple cases for strong inducts done; infrastructure for the difficult ones is there
2010-12-14 Christian Urban freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through)
2010-12-12 Christian Urban created strong_exhausts terms
2010-12-12 Christian Urban moved setify and listify functions into the library; introduced versions that have a type argument
2010-12-08 Christian Urban first tests about exhaust
2010-12-08 Christian Urban moved some code into the nominal_library
2010-12-06 Christian Urban ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
2010-11-15 Christian Urban proved that bn functions return a finite set
2010-11-15 Christian Urban fixed bug in fv function where a shallow binder binds lists of names
2010-11-14 Christian Urban merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
less more (0) tip