src/HOL/Nominal/nominal_package.ML
2005-10-29 urbanc 2005-10-29 1) have adjusted the swapping of the result type in add_datatype_i 2) have replaced map_nth_elem by Library.nth_map (there seems to be a clash with an existing nth_map somewhere - therefore the "Library")
2005-10-28 urbanc 2005-10-28 fixed case names in the weak induction principle and changed name from "induct" to "induct_weak"
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.