changeset 22565 | 2a1eef99bb6a |
parent 22562 | 80b814fe284b |
child 22578 | b0eb5652f210 |
--- a/src/HOL/Nominal/nominal_permeq.ML Tue Apr 03 16:20:34 2007 +0200 +++ b/src/HOL/Nominal/nominal_permeq.ML Tue Apr 03 17:05:52 2007 +0200 @@ -54,7 +54,6 @@ val conj_absorb = thm "conj_absorb"; val not_false = thm "not_False_eq_True" val perm_fun_def = thm "Nominal.perm_fun_def" -val swap_fun = thm "Nominal.swap_fun" (* FIXME: is this still needed? *) val perm_eq_app = thm "Nominal.pt_fun_app_eq" val supports_def = thm "Nominal.op supports_def"; val fresh_def = thm "Nominal.fresh_def";