Nominal/Nominal2.thy
2011-04-18 Christian Urban added permute_pure back into the nominal_inductive procedure; updated to Isabelle 17 April
2011-02-28 Christian Urban split the library into a basics file; merged Nominal_Eqvt into Nominal_Base
2011-01-19 Christian Urban added Minimal file to test things
2011-01-17 Christian Urban exported nominal function code to external file
2011-01-07 Christian Urban derived equivariance for the function graph and function relation
2011-01-06 Christian Urban a modified function package where, as a test, True has been injected into the compatibility condictions
2011-01-06 Christian Urban removed debugging code abd introduced a guarded tracing function
2011-01-06 Christian Urban cleaned up weakening proof and added a version with finit sets
2011-01-06 Christian Urban made sure the raw datatypes and raw functions do not get any mixfix syntax
2011-01-05 Christian Urban exported the code into a separate file
2010-12-31 Christian Urban changed res keyword to set+ for restrictions; comment by a referee
2010-12-31 Christian Urban added proper case names for all induct and exhaust theorems
2010-12-30 Christian Urban removed local fix for bug in induction_schema; added setup method for strong inductions
2010-12-28 Christian Urban automated all strong induction lemmas
2010-12-28 Christian Urban proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
2010-12-26 Christian Urban generated goals for strong induction theorems.
2010-12-23 Christian Urban moved all strong_exhaust code to nominal_dt_quot; tuned examples
2010-12-23 Christian Urban moved generic functions into nominal_library
2010-12-22 Christian Urban slight tuning
2010-12-22 Christian Urban slight tuning
2010-12-22 Christian Urban added fold_right which produces the correct term for left-infix operators
2010-12-22 Christian Urban a bit tuning
2010-12-22 Christian Urban corrected premises of strong exhausts theorems
2010-12-22 Christian Urban properly exported strong exhaust theorem; cleaned up some examples
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-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-08 Christian Urban moved definition of raw bn-functions into nominal_dt_rawfuns
2010-12-08 Christian Urban kept the nested structure of constructors (belonging to one datatype)
2010-12-07 Christian Urban automated permute_bn theorems
2010-12-06 Christian Urban moved code from nominal_dt_supp to nominal_dt_quot
2010-12-06 Christian Urban automated alpha_perm_bn theorems
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-14 Christian Urban merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
2010-11-14 Christian Urban moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
2010-11-14 Christian Urban lifted permute_bn simp rules
2010-11-13 Christian Urban lifted permute_bn constants
2010-11-13 Christian Urban respectfulness for permute_bn functions
2010-11-12 Christian Urban automated permute_bn functions (raw ones first)
2010-11-10 Christian Urban adapted to changes by Florian on the quotient package and removed local fix for function package
2010-09-29 Christian Urban worked example Foo1 with induct_schema
2010-09-27 Christian Urban added postprocessed fresh-lemmas for constructors
2010-09-27 Christian Urban post-processed eq_iff and supp threormes according to the fv-supp equality
2010-09-25 Christian Urban lifted size_thms and exported them as <name>.size
2010-09-22 Christian Urban removed dead code
2010-09-22 Christian Urban made supp proofs more robust by not using the standard induction; renamed some example files
2010-09-10 Christian Urban supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
2010-09-04 Christian Urban generated inducts rule by Project_Rule.projections
2010-09-03 Christian Urban got rid of Nominal2_Supp (is now in Nomina2_Base)
2010-08-29 Christian Urban renamed NewParser to Nominal2
less more (0) tip