Nominal/Nominal2.thy
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