diff -r 219e3ff68de8 -r fd483d8f486b Nominal/TySch.thy
--- a/Nominal/TySch.thy	Thu Mar 18 07:35:44 2010 +0100
+++ b/Nominal/TySch.thy	Thu Mar 18 07:43:44 2010 +0100
@@ -18,7 +18,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
@@ -61,13 +61,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)
@@ -77,7 +77,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)
@@ -88,7 +88,7 @@
 
 lemma
   shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))"
-  apply(simp add: t_tyS_inject)
+  apply(simp add: t_tyS_eq_iff)
   apply(rule_tac x="0::perm" in exI)
   apply(simp add: alpha_gen)
   apply(auto)
@@ -97,7 +97,7 @@
 
 lemma
   shows "All {a, b} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var b) (Var a))"
-  apply(simp add: t_tyS_inject)
+  apply(simp add: t_tyS_eq_iff)
   apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
   apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts)
   apply auto
@@ -105,18 +105,18 @@
 
 lemma
   shows "All {a, b, c} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var a) (Var b))"
-  apply(simp add: t_tyS_inject)
+  apply(simp add: t_tyS_eq_iff)
   apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_inject)
+  apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_eq_iff)
 oops
 
 lemma
   assumes a: "a \<noteq> b"
   shows "\<not>(All {a, b} (Fun (Var a) (Var b)) = All {c} (Fun (Var c) (Var c)))"
   using a
-  apply(simp add: t_tyS_inject)
+  apply(simp add: t_tyS_eq_iff)
   apply(clarify)
-  apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_inject)
+  apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_eq_iff)
   apply auto
   done