diff -r 219e3ff68de8 -r fd483d8f486b Nominal/Test.thy
--- a/Nominal/Test.thy	Thu Mar 18 07:35:44 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 18 07:43:44 2010 +0100
@@ -32,12 +32,12 @@
 apply(simp_all add: lm_fv)
 apply(simp only: supp_def)
 apply(simp only: lm_perm)
-apply(simp only: lm_inject)
+apply(simp only: lm_eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lm_perm)
-apply(simp only: lm_inject)
+apply(simp only: lm_eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
@@ -47,7 +47,7 @@
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lm_perm)
 apply(simp only: permute_ABS)
-apply(simp only: lm_inject)
+apply(simp only: lm_eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
 apply(simp only: alpha_gen)
@@ -116,7 +116,7 @@
   "bi (BP x t) = {atom x}"
 
 thm lam_bp_fv
-thm lam_bp_inject
+thm lam_bp_eq_iff
 thm lam_bp_bn
 thm lam_bp_perm
 thm lam_bp_induct
@@ -138,13 +138,13 @@
 (* VAR case *)
 apply(simp only: supp_def)
 apply(simp only: lam_bp_perm)
-apply(simp only: lam_bp_inject)
+apply(simp only: lam_bp_eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 (* APP case *)
 apply(simp only: supp_def)
 apply(simp only: lam_bp_perm)
-apply(simp only: lam_bp_inject)
+apply(simp only: lam_bp_eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
@@ -154,7 +154,7 @@
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam_bp_perm)
 apply(simp only: permute_ABS)
-apply(simp only: lam_bp_inject)
+apply(simp only: lam_bp_eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
 apply(simp only: alpha_gen)
@@ -166,7 +166,7 @@
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam_bp_perm)
 apply(simp only: permute_ABS)
-apply(simp only: lam_bp_inject)
+apply(simp only: lam_bp_eq_iff)
 apply(simp only: eqvts)
 apply(simp only: Abs_eq_iff)
 apply(simp only: ex_simps)
@@ -183,7 +183,7 @@
 (* BP case *)
 apply(simp only: supp_def)
 apply(simp only: lam_bp_perm)
-apply(simp only: lam_bp_inject)
+apply(simp only: lam_bp_eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
@@ -211,7 +211,7 @@
   "bi' (BP' x t) = {atom x}"
 
 thm lam'_bp'_fv
-thm lam'_bp'_inject[no_vars]
+thm lam'_bp'_eq_iff[no_vars]
 thm lam'_bp'_bn
 thm lam'_bp'_perm
 thm lam'_bp'_induct
@@ -227,13 +227,13 @@
 (* VAR case *)
 apply(simp only: supp_def)
 apply(simp only: lam'_bp'_perm)
-apply(simp only: lam'_bp'_inject)
+apply(simp only: lam'_bp'_eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 (* APP case *)
 apply(simp only: supp_def)
 apply(simp only: lam'_bp'_perm)
-apply(simp only: lam'_bp'_inject)
+apply(simp only: lam'_bp'_eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
@@ -243,7 +243,7 @@
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam'_bp'_perm)
 apply(simp only: permute_ABS)
-apply(simp only: lam'_bp'_inject)
+apply(simp only: lam'_bp'_eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
 apply(simp only: alpha_gen)
@@ -256,7 +256,7 @@
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam'_bp'_perm)
 apply(simp only: permute_ABS)
-apply(simp only: lam'_bp'_inject)
+apply(simp only: lam'_bp'_eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: alpha_gen)
 apply(simp only: eqvts split_def fst_conv snd_conv)
@@ -266,7 +266,7 @@
 apply blast
 apply(simp only: supp_def)
 apply(simp only: lam'_bp'_perm)
-apply(simp only: lam'_bp'_inject)
+apply(simp only: lam'_bp'_eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
@@ -299,7 +299,7 @@
 | "f (PS x) = {atom x}"
 
 thm trm'_pat'_fv
-thm trm'_pat'_inject
+thm trm'_pat'_eq_iff
 thm trm'_pat'_bn
 thm trm'_pat'_perm
 thm trm'_pat'_induct
@@ -313,13 +313,13 @@
 (* VAR case *)
 apply(simp only: supp_def)
 apply(simp only: trm'_pat'_perm)
-apply(simp only: trm'_pat'_inject)
+apply(simp only: trm'_pat'_eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 (* APP case *)
 apply(simp only: supp_def)
 apply(simp only: trm'_pat'_perm)
-apply(simp only: trm'_pat'_inject)
+apply(simp only: trm'_pat'_eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
@@ -329,7 +329,7 @@
 apply(simp (no_asm) only: supp_def)
 apply(simp only: trm'_pat'_perm)
 apply(simp only: permute_ABS)
-apply(simp only: trm'_pat'_inject)
+apply(simp only: trm'_pat'_eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
 apply(simp only: alpha_gen)
@@ -342,7 +342,7 @@
 apply(simp (no_asm) only: supp_def)
 apply(simp only: trm'_pat'_perm)
 apply(simp only: permute_ABS)
-apply(simp only: trm'_pat'_inject)
+apply(simp only: trm'_pat'_eq_iff)
 apply(simp only: eqvts)
 apply(simp only: Abs_eq_iff)
 apply(simp only: ex_simps)
@@ -359,19 +359,19 @@
 (* PN case *)
 apply(simp only: supp_def)
 apply(simp only: trm'_pat'_perm)
-apply(simp only: trm'_pat'_inject)
+apply(simp only: trm'_pat'_eq_iff)
 apply(simp)
 (* PS case *)
 apply(simp only: supp_def)
 apply(simp only: trm'_pat'_perm)
-apply(simp only: trm'_pat'_inject)
+apply(simp only: trm'_pat'_eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 apply(simp)
 (* PD case *)
 apply(simp only: supp_def)
 apply(simp only: trm'_pat'_perm)
-apply(simp only: trm'_pat'_inject)
+apply(simp only: trm'_pat'_eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
@@ -399,7 +399,7 @@
 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
 
 thm trm0_pat0_fv
-thm trm0_pat0_inject
+thm trm0_pat0_eq_iff
 thm trm0_pat0_bn
 thm trm0_pat0_perm
 thm trm0_pat0_induct
@@ -414,7 +414,7 @@
   All xs::"name set" ty::"t" bind xs in ty
 
 thm t_tyS_fv
-thm t_tyS_inject
+thm t_tyS_eq_iff
 thm t_tyS_bn
 thm t_tyS_perm
 thm t_tyS_induct
@@ -448,13 +448,13 @@
 (* VarTS case *)
 apply(simp only: supp_def)
 apply(simp only: t_tyS_perm)
-apply(simp only: t_tyS_inject)
+apply(simp only: t_tyS_eq_iff)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
 (* FunTS case *)
 apply(simp only: supp_def)
 apply(simp only: t_tyS_perm)
-apply(simp only: t_tyS_inject)
+apply(simp only: t_tyS_eq_iff)
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
@@ -464,7 +464,7 @@
 apply(simp (no_asm) only: supp_def)
 apply(simp only: t_tyS_perm)
 apply(simp only: permute_ABS)
-apply(simp only: t_tyS_inject)
+apply(simp only: t_tyS_eq_iff)
 apply(simp only: Abs_eq_iff)
 apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw)
 apply(simp only: alpha_gen)
@@ -495,7 +495,7 @@
 | "bv1 (BV1 x) = {atom x}"
 
 thm trm1_bp1_fv
-thm trm1_bp1_inject
+thm trm1_bp1_eq_iff
 thm trm1_bp1_bn
 thm trm1_bp1_perm
 thm trm1_bp1_induct
@@ -518,7 +518,7 @@
 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
 
 thm trm3_rassigns3_fv
-thm trm3_rassigns3_inject
+thm trm3_rassigns3_eq_iff
 thm trm3_rassigns3_bn
 thm trm3_rassigns3_perm
 thm trm3_rassigns3_induct
@@ -545,7 +545,7 @@
 | "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
 
 thm trm5_lts_fv
-thm trm5_lts_inject
+thm trm5_lts_eq_iff
 thm trm5_lts_bn
 thm trm5_lts_perm
 thm trm5_lts_induct
@@ -565,7 +565,7 @@
 |  ImpR c::"coname" n::"name" t::"phd" "coname"                 bind n in t, bind c in t
 
 thm phd_fv
-thm phd_inject
+thm phd_eq_iff
 thm phd_bn
 thm phd_perm
 thm phd_induct
@@ -625,7 +625,7 @@
 | "Cbinders (SVal v T) = {atom v}"
 
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_fv
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_inject
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_eq_iff
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_bn
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_perm
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_induct
@@ -651,7 +651,7 @@
 | "bp'' (PPair p1 p2) = bp'' p1 \<union> bp'' p2"
 
 thm exp_pat3_fv
-thm exp_pat3_inject
+thm exp_pat3_eq_iff
 thm exp_pat3_bn
 thm exp_pat3_perm
 thm exp_pat3_induct
@@ -674,7 +674,7 @@
 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
 
 thm exp6_pat6_fv
-thm exp6_pat6_inject
+thm exp6_pat6_eq_iff
 thm exp6_pat6_bn
 thm exp6_pat6_perm
 thm exp6_pat6_induct