src/HOL/Nominal/nominal_package.ML
2005-10-28 berghofe 2005-10-28 Implemented proof of weak induction theorem.
2005-10-28 berghofe 2005-10-28 Removed legacy prove_goalw_cterm command.
2005-10-17 berghofe 2005-10-17 Improved proof of injectivity theorems to make it work on "ordinary" function types as well.
2005-10-17 berghofe 2005-10-17 Fixed bug in proof of support theorem (it failed on constructors with no arguments).
2005-10-17 berghofe 2005-10-17 Implemented proofs for support and freshness theorems.
2005-10-17 berghofe 2005-10-17 Initial revision.